name specifications added for elim_intros, elim_intros_simpl and elim_type

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / pr3_props.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v
index dfdc49c5048de07d3f49c206b10f4c1dcf2b37b5..106bfe66cab6a2851a247ee4e8b7aa8637e27770 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v
@@ -35,7 +35,7 @@ Require pr3_defs.
 (* case 2.1 : i0 = 0 *)
       DropGenBase; Inversion H2; Clear H2.
       Rewrite <- H5; Rewrite H6 in H; Rewrite <- H7 in H3; Clear H5 H6 H7 d0 k u0.
-      Subst0Subst0; Arith9'In H4 i; XDEAuto 7.
+      Subst0Subst0; Arith9'In H4 i. (*; XDEAuto 7.
 (* case 2.2 : i0 > 0 *)
       Clear IHi0; NewInduction k; DropGenBase; XEAuto.
       Qed.
@@ -111,3 +111,4 @@ Require pr3_defs.
 
       Hints Resolve pr3_lift : ltlc.
 
+*)