Safer, though ad hoc, approach to re-interpretation of the argument of

general_multi_multi_rewrite. Due to the option "!" of rewrite, a lemma
may need to be interpreted several times with different instances of
the implicit arguments. Interpreting the term as a constr in
tacinterp.ml would need to either refresh the holes (i.e. the evars)
or detype what has been typed and in both cases, complicated things
can happen because the evars associated to these holes may have been
used in instantiating former evars of the goal. Leaving the term as a
rawconstr would need to export the interpretation functions from
tacinterp which is technically complicated in the current situation
because equality.ml is currently linked before tacinterp. The solution
used is to delay the interpretation using an ML closure.



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

3 files changed, 14 insertions, 8 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 62581d74b2..23966b6c29 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -329,11 +329,14 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
 	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) true ?tac c with_evars)
 	   do_hyps
 
+type delayed_open_constr_with_bindings =
+    env -> evar_map -> evar_map * constr with_bindings
+
 let general_multi_multi_rewrite with_evars l cl tac =
-  let do1 l2r c gl =
+  let do1 l2r f gl =
+    let sigma,c = f (pf_env gl) (project gl) in
     Refiner.tclWITHHOLES with_evars
-      (general_multi_rewrite l2r with_evars ?tac c.it)
-      (Evd.merge (project gl) c.sigma) cl gl in
+      (general_multi_rewrite l2r with_evars ?tac c) sigma cl gl in
   let rec doN l2r c = function
     | Precisely n when n <= 0 -> tclIDTAC
     | Precisely 1 -> do1 l2r c
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 9986d230bb..b5c147393d 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -68,9 +68,13 @@ val general_rewrite_in          :
 
 val general_multi_rewrite :
   orientation -> evars_flag -> ?tac:(tactic * conditions) -> constr with_bindings -> clause -> tactic
+
+type delayed_open_constr_with_bindings =
+    env -> evar_map -> evar_map * constr with_bindings
+
 val general_multi_multi_rewrite :
-  evars_flag -> (bool * multi * constr with_bindings sigma) list -> clause ->
-  (tactic * conditions) option -> tactic
+  evars_flag -> (bool * multi * delayed_open_constr_with_bindings) list -> 
+    clause -> (tactic * conditions) option -> tactic
 
 val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic
 val replace    : constr -> constr -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 719fa7f859..85986503ed 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2417,9 +2417,8 @@ and interp_atomic ist gl tac =
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) ->
       let l = List.map (fun (b,m,c) ->
-        let sigma',c = interp_open_constr_with_bindings ist env sigma c in
-        let _,sigma' = Evarutil.subtract_evars sigma sigma' in
-        (b,m,{it=c;sigma=sigma'})) l in
+        let f env sigma = interp_open_constr_with_bindings ist env sigma c in
+	(b,m,f)) l in
       let cl = interp_clause ist gl cl in
       Equality.general_multi_multi_rewrite ev l cl
         (Option.map (fun by -> tclCOMPLETE (interp_tactic ist by), Equality.Naive) by)