Move out JMeq of subst for compatibility (it affects e.g. the

compilation of Grenoble/ATBR). Add subst' for subst extended with JMeq
(maybe an option would be better??).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12264 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 15 insertions, 5 deletions

diff --git a/CHANGES b/CHANGES
index 0688f52463..7066043049 100644
--- a/CHANGES
+++ b/CHANGES
@@ -26,6 +26,7 @@ Tactics
   new option "Unset Tactic Evars Pattern Unification" to deactivate it.
 - New tactic "etransitivity".
 - Support of JMeq for "injection" and "discriminate".
+- New variant "subst'" of "subst" that supports JMeq.
 
 Tactic Language
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 01e5efc70c..699f334412 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1208,6 +1208,9 @@ let unfold_body x gl =
 
 
 
+let restrict_to_eq_and_identity eq = (* compatibility *)
+  if eq <> constr_of_global glob_eq && eq <> constr_of_global glob_identity then
+    raise PatternMatchingFailure
 
 exception FoundHyp of (identifier * constr * bool)
 
@@ -1220,7 +1223,7 @@ let is_eq_x gl x (id,_,c) =
   with PatternMatchingFailure ->
     ()
 
-let subst_one x gl = 
+let subst_one x gl =
   let hyps = pf_hyps gl in
   let (_,xval,_) = pf_get_hyp gl x in
   (* If x has a body, simply replace x with body and clear x *)
@@ -1275,10 +1278,11 @@ let subst_one x gl =
 
 let subst ids = tclTHEN tclNORMEVAR (tclMAP subst_one ids)
 
-let subst_all gl =
+let subst_all ?(strict=true) gl =
   let test (_,c) =
     try
-      let (_,x,y) = snd (find_eq_data_decompose gl c) in
+      let lbeq,(_,x,y) = find_eq_data_decompose gl c in
+      if strict then restrict_to_eq_and_identity lbeq.eq;
       (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
       if eq_constr x y then failwith "caught";
       match kind_of_term x with Var x -> x | _ -> 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index a52d064996..d694491b95 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -129,7 +129,7 @@ val injectable : env -> evar_map -> constr -> constr -> bool
 val unfold_body : identifier -> tactic
 
 val subst : identifier list -> tactic
-val subst_all : tactic
+val subst_all : ?strict:bool -> tactic
 
 (* Replace term *)
 (* [replace_multi_term dir_opt c cl] 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 2b4b9cffe9..f1c2551548 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -335,7 +335,12 @@ END
 
 TACTIC EXTEND subst
 | [ "subst" ne_var_list(l) ] -> [ subst l ]
-| [ "subst" ] -> [ subst_all ]
+| [ "subst" ] -> [ subst_all ~strict:true] (* W/o JMeq *)
+
+END
+
+TACTIC EXTEND subst'
+| [ "subst'" ] -> [ subst_all ~strict:false ] (* With JMeq *)
 END
 
 open Evar_tactics