coq-community · Casteran · Jan 25, 2022 · Jan 24, 2022 · Jan 24, 2022 · Jan 24, 2022
diff --git a/theories/ordinals/Ackermann/Deduction.v b/theories/ordinals/Ackermann/Deduction.v
@@ -1,4 +1,3 @@
-Set Apply With Renaming.
 
 Require Import Ensembles.
 Require Import Coq.Lists.List.

diff --git a/theories/ordinals/Ackermann/LNN.v b/theories/ordinals/Ackermann/LNN.v
@@ -1,4 +1,3 @@
-Set Apply With Renaming.
 
 Require Import Arith.
 Require Import Ensembles.

diff --git a/theories/ordinals/Ackermann/LNN2LNT.v b/theories/ordinals/Ackermann/LNN2LNT.v
@@ -1,4 +1,3 @@
-Set Apply With Renaming.
 
 Require Import Ensembles.
 Require Import Coq.Lists.List.

diff --git a/theories/ordinals/Ackermann/LNT.v b/theories/ordinals/Ackermann/LNT.v
@@ -1,4 +1,3 @@
-Set Apply With Renaming.
 
 Require Import Arith.
 Require Import Ensembles.

diff --git a/theories/ordinals/Ackermann/Languages.v b/theories/ordinals/Ackermann/Languages.v
@@ -1,4 +1,3 @@
-Set Apply With Renaming.
 
 Require Import Arith.
 Require Import fol.

diff --git a/theories/ordinals/Ackermann/ListExt.v b/theories/ordinals/Ackermann/ListExt.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import Coq.Lists.List.
 
 Section List_Remove.

diff --git a/theories/ordinals/Ackermann/NN.v b/theories/ordinals/Ackermann/NN.v
@@ -1,4 +1,3 @@
-Set Apply With Renaming.
 
 Require Import Arith.
 Require Import Ensembles.

diff --git a/theories/ordinals/Ackermann/NN2PA.v b/theories/ordinals/Ackermann/NN2PA.v
@@ -1,4 +1,3 @@
-Set Apply With Renaming.
 
 Require Import Ensembles.
 Require Import Coq.Lists.List.

diff --git a/theories/ordinals/Ackermann/NNtheory.v b/theories/ordinals/Ackermann/NNtheory.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import Arith.
 
 Require Import folLogic3.

diff --git a/theories/ordinals/Ackermann/PA.v b/theories/ordinals/Ackermann/PA.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import Arith.
 Require Import Ensembles.
 

diff --git a/theories/ordinals/Ackermann/PAconsistent.v b/theories/ordinals/Ackermann/PAconsistent.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import Arith.
 Require Import folProof.
 Require Import folProp.

diff --git a/theories/ordinals/Ackermann/PAtheory.v b/theories/ordinals/Ackermann/PAtheory.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import Ensembles.
 Require Import Coq.Lists.List.
 Require Import Arith.

diff --git a/theories/ordinals/Ackermann/cPair.v b/theories/ordinals/Ackermann/cPair.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import Arith.
 Require Import Coq.Lists.List.
 Require Import extEqualNat.

diff --git a/theories/ordinals/Ackermann/checkPrf.v b/theories/ordinals/Ackermann/checkPrf.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import primRec.
 Require Import codeFreeVar.
 Require Import codeSubFormula.

diff --git a/theories/ordinals/Ackermann/code.v b/theories/ordinals/Ackermann/code.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import Arith.
 Require Import fol.
 Require Import folProof.

diff --git a/theories/ordinals/Ackermann/codeFreeVar.v b/theories/ordinals/Ackermann/codeFreeVar.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import primRec.
 Require Import cPair.
 Require Import Coq.Lists.List.

diff --git a/theories/ordinals/Ackermann/codeList.v b/theories/ordinals/Ackermann/codeList.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import primRec.
 Require Import cPair.
 Require Export Coq.Lists.List.

diff --git a/theories/ordinals/Ackermann/codeNatToTerm.v b/theories/ordinals/Ackermann/codeNatToTerm.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import primRec.
 Require Import cPair.
 Require Import Arith.

diff --git a/theories/ordinals/Ackermann/codePA.v b/theories/ordinals/Ackermann/codePA.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import Ensembles.
 Require Import Coq.Lists.List.
 Require Import primRec.

diff --git a/theories/ordinals/Ackermann/codeSubFormula.v b/theories/ordinals/Ackermann/codeSubFormula.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import primRec.
 Require Import cPair.
 Require Import Arith.

diff --git a/theories/ordinals/Ackermann/codeSubTerm.v b/theories/ordinals/Ackermann/codeSubTerm.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import primRec.
 Require Import cPair.
 Require Import Arith.

diff --git a/theories/ordinals/Ackermann/expressible.v b/theories/ordinals/Ackermann/expressible.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import Arith.
 Require Import Coq.Lists.List.
 Require Import ListExt.

diff --git a/theories/ordinals/Ackermann/extEqualNat.v b/theories/ordinals/Ackermann/extEqualNat.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import Arith.
 
 (* begin snippet naryFunc *)

diff --git a/theories/ordinals/Ackermann/fol.v b/theories/ordinals/Ackermann/fol.v
@@ -1,8 +1,6 @@
 (* Author: Russell O'Connor *)
 (* This file is Public Domain *)
 
-Set Apply With Renaming.
-
 Require Import Coq.Lists.List.
 Require Import Ensembles.
 Require Import Peano_dec.
@@ -34,7 +32,8 @@ Scheme Term_Terms_rec := Minimality for Term Sort Set
 
 Scheme Term_Terms_rec_full := Induction for Term
   Sort Set
-  with Terms_Term_rec_full := Induction for Terms Sort Set.
+    with Terms_Term_rec_full := Induction for Terms Sort Set.
+
 
 Inductive Formula : Set :=
   | equal : Term -> Term -> Formula
@@ -133,6 +132,8 @@ simpl in H0.
 apply (H0 (refl_equal (S n))).
 Qed.
 
+Arguments Term_Terms_rec_full P P0: rename.
+
 Lemma term_dec : forall x y : Term, {x = y} + {x <> y}.
 Proof.
 induction language_dec.
@@ -791,3 +792,16 @@ Qed.
 End Formula_Depth_Induction.
 
 End First_Order_Logic.
+
+
+Arguments Term_Terms_ind  L P P0 : rename.
+Arguments Terms_Term_ind L P P0 : rename.
+
+Arguments Term_Terms_rec L P P0 : rename.
+Arguments Terms_Term_rec L P P0 : rename.
+
+Arguments Term_Terms_rec_full L P P0 : rename.
+Arguments Terms_Term_rec_full L P P0 : rename.
+
+
+
diff --git a/theories/ordinals/Ackermann/folLogic.v b/theories/ordinals/Ackermann/folLogic.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import Ensembles.
 Require Import Coq.Lists.List.
 

diff --git a/theories/ordinals/Ackermann/folLogic2.v b/theories/ordinals/Ackermann/folLogic2.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import Ensembles.
 Require Import Coq.Lists.List.
 Require Import ListExt.

diff --git a/theories/ordinals/Ackermann/folLogic3.v b/theories/ordinals/Ackermann/folLogic3.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import Ensembles.
 Require Import Coq.Lists.List.
 Require Import ListExt.

diff --git a/theories/ordinals/Ackermann/folProof.v b/theories/ordinals/Ackermann/folProof.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import Ensembles.
 Require Import Coq.Lists.List.
 Require Import Arith.

diff --git a/theories/ordinals/Ackermann/folProp.v b/theories/ordinals/Ackermann/folProp.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import Wf_nat.
 Require Import Max.
 Require Import Arith.

diff --git a/theories/ordinals/Ackermann/folReplace.v b/theories/ordinals/Ackermann/folReplace.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import Ensembles.
 Require Import Coq.Lists.List.
 Require Import Peano_dec.

diff --git a/theories/ordinals/Ackermann/misc.v b/theories/ordinals/Ackermann/misc.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import Eqdep_dec.
 
 Global Set Asymmetric Patterns.

diff --git a/theories/ordinals/Ackermann/model.v b/theories/ordinals/Ackermann/model.v
@@ -1,6 +1,3 @@
-Set Apply With Renaming.
-
-
 Require Import Ensembles.
 Require Import Coq.Lists.List.
 Require Import ListExt.

diff --git a/theories/ordinals/Ackermann/prLogic.v b/theories/ordinals/Ackermann/prLogic.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import primRec.
 Require Import code.
 Require Import Arith.

diff --git a/theories/ordinals/Ackermann/primRec.v b/theories/ordinals/Ackermann/primRec.v
@@ -1,6 +1,5 @@
 (** Primitive Recursive functions *)
 (** Russel O'Connor *)
-Set Apply With Renaming.
 
 Require Import Arith.
 Require Import Peano_dec.
@@ -44,10 +43,16 @@ with PrimRecs : nat -> nat -> Set :=
 Scheme PrimRec_PrimRecs_rec := Induction for PrimRec Sort Set
   with PrimRecs_PrimRec_rec := Induction for PrimRecs  Sort Set.
 
+Arguments PrimRec_PrimRecs_rec P P0 : rename.
+Arguments PrimRecs_PrimRec_rec P P0 : rename.
+
 (* begin snippet SchemePrimRecInd *)
 
 Scheme PrimRec_PrimRecs_ind := Induction for PrimRec Sort Prop
-  with PrimRecs_PrimRec_ind := Induction for PrimRecs  Sort Prop.
+    with PrimRecs_PrimRec_ind := Induction for PrimRecs  Sort Prop.
+
+Arguments PrimRec_PrimRecs_ind P P0 : rename.
+Arguments PrimRecs_PrimRec_ind P P0 : rename.
 (* end snippet SchemePrimRecInd *)
 
 (* begin snippet SchemePrimRecInda *)

diff --git a/theories/ordinals/Ackermann/subAll.v b/theories/ordinals/Ackermann/subAll.v
@@ -1,4 +1,3 @@
-Set Apply With Renaming.
 
 Require Import Ensembles.
 Require Import Coq.Lists.List.

diff --git a/theories/ordinals/Ackermann/subProp.v b/theories/ordinals/Ackermann/subProp.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import Ensembles.
 Require Import Coq.Lists.List.
 Require Import Peano_dec.

diff --git a/theories/ordinals/Ackermann/wConsistent.v b/theories/ordinals/Ackermann/wConsistent.v
@@ -1,5 +1,3 @@
-Set Apply With Renaming.
-
 Require Import folProof.
 Require Import Arith.
 Require Import folProp.

diff --git a/theories/ordinals/Ackermann/wellFormed.v b/theories/ordinals/Ackermann/wellFormed.v
@@ -1,4 +1,3 @@
-Set Apply With Renaming.
 
 Require Import primRec.
 Require Import cPair.

diff --git a/theories/ordinals/Hydra/Hydra_Definitions.v b/theories/ordinals/Hydra/Hydra_Definitions.v
@@ -42,6 +42,10 @@ Scheme Hydra_rect2 := Induction for Hydra Sort Type
 with   Hydrae_rect2 := Induction for Hydrae Sort Type.
 (* end snippet HydraRect2 *)
 
+Arguments Hydra_rect2 P P0 : rename.
+Arguments Hydrae_rect2 P P0 : rename.
+
+
 (* begin snippet hForall *)
 (** All elements of s satisfy P *)
 Fixpoint h_forall (P: Hydra -> Prop) (s: Hydrae) :=

diff --git a/theories/ordinals/Hydra/Hydra_Lemmas.v b/theories/ordinals/Hydra/Hydra_Lemmas.v
@@ -111,6 +111,8 @@ Qed.
 Scheme R2_ind2 := Induction for R2 Sort Prop
                   with
                   S2_ind2 := Induction for S2 Sort Prop.
+Arguments  R2_ind2 n P P0 : rename.
+Arguments  S2_ind2 n P P0 : rename.
 
 Lemma S2_app : forall  n  s1 s2 ,
     S2 n s1 s2 ->