Merge pull request #125 from proux01/mc1456

Adapt to math-comp/math-comp#1456

Author: proux01

examples/field_examples.v

@@ -2,7 +2,7 @@
 (* `field_examples_no_check.v`. To edit this file, uncomment `Require         *)
 (* Import`s below: *)
 (* From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat. *)
-(* From mathcomp Require Import ring. *)
+(* From mathcomp.algebra_tactics Require Import ring. *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.

examples/field_examples_check.v

@@ -1,4 +1,4 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
-From mathcomp Require Import ring.
+From mathcomp.algebra_tactics Require Import ring.
 
 Load "field_examples.v".

examples/field_examples_no_check.v

@@ -1,5 +1,5 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
-From mathcomp Require Import ring.
+From mathcomp.algebra_tactics Require Import ring.
 
 Ltac field_reflection ::= field_reflection_no_check.
 

examples/from_sander.v

@@ -1,5 +1,5 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
-From mathcomp Require Import ring.
+From mathcomp.algebra_tactics Require Import ring.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

examples/ring_error.v

@@ -1,5 +1,5 @@
 From mathcomp Require Import all_ssreflect ssralg.
-From mathcomp Require Import ring.
+From mathcomp.algebra_tactics Require Import ring.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

examples/ring_examples.v

@@ -1,8 +1,8 @@
 (* This file should be tested by loaded from `ring_examples_check.v` and      *)
 (* `ring_examples_no_check.v`. To edit this file, uncomment `Require Import`s *)
 (* below: *)
-(* From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat. *)
-(* From mathcomp Require Import ring ssrZ. *)
+(* From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat ssrZ. *)
+(* From mathcomp.algebra_tactics Require Import ring. *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.

examples/ring_examples_check.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
-From mathcomp Require Import ring ssrZ.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat ssrZ.
+From mathcomp.algebra_tactics Require Import ring.
 
 Load "ring_examples.v".

examples/ring_examples_no_check.v

@@ -1,5 +1,5 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
-From mathcomp Require Import ring ssrZ.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat ssrZ.
+From mathcomp.algebra_tactics Require Import ring.
 
 Ltac ring_reflection ::= ring_reflection_no_check.