CPDT Coq 8.13 patch

cpdt-coq-8.13.patch

--- cpdt/src/DataStruct.v	2020-02-02 12:46:14.000000000 -0300
+++ cpdt-8.13/src/DataStruct.v	2021-12-05 11:05:01.000000000 -0300
@@ -117,8 +117,8 @@
 (* end thide *)
 End ilist.
 
-Arguments Nil [A].
-Arguments First [n].
+Arguments Nil {A}.
+Arguments First {n}.
 
 (** A few examples show how to make use of these definitions. *)
 
@@ -242,11 +242,11 @@
 End hlist.
 
 (* begin thide *)
-Arguments HNil [A B].
-Arguments HCons [A B x ls] _ _.
+Arguments HNil {A B}.
+Arguments HCons {A B x ls} _ _.
 
-Arguments HFirst [A elm ls].
-Arguments HNext [A elm x ls] _.
+Arguments HFirst {A elm ls}.
+Arguments HNext {A elm x ls} _.
 (* end thide *)
 
 (** By putting the parameters [A] and [B] in [Type], we enable fancier kinds of polymorphism than in mainstream functional languages.  For instance, one use of [hlist] is for the simple heterogeneous lists that we referred to earlier. *)
@@ -302,7 +302,7 @@
 | Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran).
 (* end thide *)
 
-Arguments Const [ts].
+Arguments Const {ts}.
 
 (** We write a simple recursive function to translate [type]s into [Set]s. *)
 
--- cpdt/src/DepList.v	2020-02-02 12:46:14.000000000 -0300
+++ cpdt-8.13/src/DepList.v	2021-12-05 10:57:29.000000000 -0300
@@ -107,8 +107,8 @@
   End fold.
 End ilist.
 
-Arguments INil [A].
-Arguments First [n].
+Arguments INil {A}.
+Arguments First {n}.
 
 Section imap.
   Variables A B : Type.
@@ -197,12 +197,12 @@
   Qed.
 End hlist.
 
-Arguments HNil [A B].
-Arguments HCons [A B x ls] _ _.
-Arguments hmake [A B] f ls.
+Arguments HNil {A B}.
+Arguments HCons {A B x ls} _ _.
+Arguments hmake {A B} f ls.
 
-Arguments HFirst [A elm ls].
-Arguments HNext [A elm x ls] _.
+Arguments HFirst {A elm ls}.
+Arguments HNext {A elm x ls} _.
 
 Infix ":::" := HCons (right associativity, at level 60).
 Infix "+++" := happ (right associativity, at level 60).
--- cpdt/src/InductiveTypes.v	2020-02-02 12:46:14.000000000 -0300
+++ cpdt-8.13/src/InductiveTypes.v	2021-12-05 11:01:49.000000000 -0300
@@ -479,7 +479,7 @@
 (* end thide *)
 End list.
 
-Arguments Nil [T].
+Arguments Nil {T}.
 
 (** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed.  With an [Arguments]%~\index{Vernacular commands!Arguments}% command, we ask that [T] be inferred when we use [Nil]; Coq's heuristics already decided to apply a similar policy to [Cons], because of the [Set Implicit Arguments]%~\index{Vernacular commands!Set Implicit Arguments}% command elided at the beginning of this chapter.  We verify that our definitions have been saved properly using the [Print] command, a cousin of [Check] which shows the definition of a symbol, rather than just its type. *)
 
--- cpdt/src/Large.v	2020-02-02 12:46:14.000000000 -0300
+++ cpdt-8.13/src/Large.v	2021-12-05 11:13:14.000000000 -0300
@@ -260,7 +260,7 @@
 
    The [crush] tactic does not know how to finish this goal.  We could finish the proof manually. *)
 
-  rewrite <- IHe2; crush.
+  (* rewrite <- IHe2; crush. *)
 
   (** However, the proof would be easier to understand and maintain if we separated this insight into a separate lemma. *)
 
@@ -460,7 +460,6 @@
   (** What is [t] doing to get us to this point?  The %\index{tactics!info}%[info] command can help us answer this kind of question.  (As of this writing, [info] is no longer functioning in the most recent Coq release, but I hope it returns.) *)
 
   Undo.
-  info t.
 
   (* begin hide *)
   (* begin thide *)
@@ -515,7 +514,6 @@
 
   Undo.
 
-  info autorewrite with core in *.
   (** %\vspace{-.15in}%[[
  == refine (eq_ind_r (fun n : nat => n = eval e1 * eval e2) _
               (confounder (reassoc e1) e3 e4)).
@@ -566,7 +564,6 @@
 
 (* begin thide *)
     Restart.
-    info eauto 6.
     (** %\vspace{-.15in}%[[
  == intro x; intro y; intro H; intro H0; intro H4;
        simple eapply trans_eq.
--- cpdt/src/LogicProg.v	2020-02-02 12:46:14.000000000 -0300
+++ cpdt-8.13/src/LogicProg.v	2021-12-05 11:06:57.000000000 -0300
@@ -152,7 +152,7 @@
 (** Sometimes it is useful to see a description of the proof tree that [auto] finds, with the %\index{tactics!info}%[info] tactical.  (This tactical is not available in Coq 8.4 as of this writing, but I hope it reappears soon.  The special case %\index{tactics!info\_auto}%[info_auto] tactic is provided as a chatty replacement for [auto].) *)
 
 Restart.
-  info auto 6.
+  info_auto 6.
 (** %\vspace{-.15in}%[[
  == apply PlusS; apply PlusS; apply PlusS; apply PlusS; 
     apply PlusS; apply PlusO.
@@ -220,7 +220,7 @@
 (** The [auto] tactic will not perform these sorts of steps that introduce unification variables, but the %\index{tactics!eauto}%[eauto] tactic will.  It is helpful to work with two separate tactics, because proof search in the [eauto] style can uncover many more potential proof trees and hence take much longer to run. *)
 
 Restart.
-  info eauto 6.
+  info_eauto 6.
 (** %\vspace{-.15in}%[[
  == eapply ex_intro; apply PlusS; apply PlusS; 
     apply PlusS; apply PlusS; apply PlusO.
@@ -431,7 +431,7 @@
   -> y = 2
   -> exists z, z + x = 3.
 (* begin thide *)
-  info eauto with slow.
+  info_eauto with slow.
 (** %\vspace{-.2in}%[[
  == intro x; intro y; intro H; intro H0; simple eapply ex_intro; 
     apply plusS; simple eapply eq_trans.