Last attempt to adapt to stdlib's changes

coq-community · Jan 2, 2024 · fb855a7 · fb855a7
1 parent 2ccd85a
commit fb855a7
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 4 deletions.
diff --git a/tutorial_inductive_co_inductive_types/SRC/RecTutorial.v b/tutorial_inductive_co_inductive_types/SRC/RecTutorial.v
@@ -747,7 +747,6 @@ Defined.
 Print Acc.
 
 
-Require Import Minus.
 
 (*
 Fixpoint div (x y:nat){struct x}: nat :=

diff --git a/tutorial_type_classes/SRC/Monoid_op_classes.v b/tutorial_type_classes/SRC/Monoid_op_classes.v
@@ -5,7 +5,7 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith   Recdef  Mat.
+Require Import ZArith Recdef  Mat.
 
 
 Class monoid_binop (A:Type) := monoid_op : A -> A -> A.
@@ -123,8 +123,7 @@ Definition tail_recursive_power  `{M : Monoid}(x:A)(n:nat) :=
 
 (* Todo:  Fix Div2 deprecation *)
 
-Require
-  Recdef  Nat.
+Require Recdef  Nat.
-Original file line number
+Diff line change
@@ Expand Up / @@ -747,7 +747,6 @@ Defined. @@
     Print Acc.
-    Require Import Minus.
     (*
     Fixpoint div (x y:nat){struct x}: nat :=
@@ Expand Down @@