Un plugging especialize because it does not work in coq-8.18.

This is due to coq's specialilze being less permissive with evars.
I Will try to find a way to reimplement when I have time. This may need
to extend coq.

Demo/demo.v

@@ -127,25 +127,29 @@ Proof.
      premiss of a hyp, and then re-quantifies everything non
      instantiated. *)
   Undo.
-  especialize H3 at 1.
+  (* THIS IS BROKEN IN COQ 8.18 *)
+  (* especialize H3 at 1.
   { apply le_S.
     apply le_n. }
-  Undo 5.
+  Undo 5. *)
   (* IDEs don't like Undo, replay the next ocommand twice will resync
      proofgeneral. *)
   (* It accepts several (up to 7) premisses numers. *)
-  especialize H3 at 2,3.
-  Undo.
+  (* BROKEN IN 8.18 *)
+  (* especialize H3 at 2,3.
+  Undo. *)
 
   (* you can ask a goal for all premisses, in the spirit of the
      "exploit" tactic from CompCert. *)
-  especialize H3 at *.
-  Undo.
+  (* BROKEN IN 8.18 *)
+  (* especialize H3 at *.
+  Undo. *)
 
   (* You can also specify that you want to instantiate the n first premisses. *)
-  especialize H3 until 3.
+  (* BROKEN IN 8.18 *)
+  (* especialize H3 until 3.
   Show 4.
-  Undo.
+  Undo. *)
 
   (* VARIABLES MIXED WITH HYPOTHESIS. *)
   (* move_up_types X. moves X at top near something of the same type,

LibHyps/LibHypsRegression.v

@@ -118,7 +118,8 @@ Lemma dummy: forall x y,
 Qed. 
 
 
-
+(* BROKEN IN 8.18 *)
+(*
 Definition eq_one (i:nat) := i = 1.
 (* eq_one is delta_reducible but I don't want it to be reduced. *)
 Lemma test_espec: (eq_one 2 -> eq_one 3 -> eq_one 1 -> False) -> True.
@@ -404,7 +405,7 @@ Proof.
   Undo.
   exact I.
 Qed.
-
+*)
 
 Require Import LibHyps.LibDecomp.
 

LibHyps/LibHypsTest.v

@@ -604,10 +604,12 @@ Proof.
   intros /s/n/g.
 
   (* Let us instantiate the 2nd premis of h_all_eq_add_add without copying its type: *)
-  especialize h_all_eq_add_add_ at 2.
+  (* BROKEN IN COQ 8.18 *)
+  (* especialize h_all_eq_add_add_ at 2.
   { apply Nat.add_0_l. }
   (* now h_all_eq_add_add is specialized *)
-  Undo 6.
+  Undo 6. *)
+  Undo 2.
   intros until 1.
   (** The taticals apply after any tactic. Notice how H:x=y is not new
     and hence not substituted, whereas z = b + x is. *)

README.md

@@ -12,7 +12,10 @@ a new tactic `especialize H` and a set of tacticals to appy or iterate
 tactics either on all hypothesis of a goal or on "new' hypothesis after
 a tactic. It also provide syntax for a few predefined such iterators.
 
-## QUICK REF: especialize
+## QUICK REF: especialize (BROKEN IN COQ-8.18)
+
+This tactic is currently broken in coq v8.18. I am working on it. This
+may need some work on coq side.
 
 + `especialize H at n [as h].` Creates a subgoal to prove the nth
     dependent premise of `H`, creating necessary evars for non
@@ -129,10 +132,12 @@ Proof.
   intros /s/n/g.
 
   (* Let us instantiate the 2nd premis of h_all_eq_add_add without copying its type: *)
-  especialize h_all_eq_add_add_ at 2.
+  (* BROKEN IN COQ 8.18*)
+  (* especialize h_all_eq_add_add_ at 2.
   { apply Nat.add_0_l. }
   (* now h_all_eq_add_add is specialized *)
-  Undo 6.
+  Undo 6. *)
+  Undo 2.
   intros until 1.
   (** The taticals apply after any tactic. Notice how H:x=y is not new
     and hence not substituted, whereas z = b + x is. *)

_CoqProject

@@ -2,7 +2,12 @@
 
 LibHyps/LibHypsNaming.v
 LibHyps/LibHypsTactics.v
-LibHyps/LibSpecialize.v
 LibHyps/LibDecomp.v
 LibHyps/TacNewHyps.v
 LibHyps/LibHyps.v
+
+# especialize is broken in coq-8.18. This is due to a change in
+# specialize tactic that does not allow new evars remaining in its
+# subgoals. This is unfortunate and hopefully fixed in the next
+# version.
+# LibHyps/LibSpecialize.v