Tentative API fix for tactic arguments to be fed to tclWITHHOLES.

The previous implementation was a source of evar leaks if misused, as
it created values coming together with their current evar_map. This is
dead wrong if the value is not used on the spot. To fix this, we rather
return a ['a delayed_open] object.

Two argument types were modified: bindings and constr_bindings. The
open_constr argument should also be fixed, but it is more entangled and
thus I leave it for another commit.

9 files changed, 42 insertions, 38 deletions

diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index f2f314eea0..052e4ec69b 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -55,12 +55,12 @@ val wit_open_constr :
 val wit_constr_with_bindings :
   (constr_expr with_bindings,
   glob_constr_and_expr with_bindings,
-  constr with_bindings Evd.sigma) genarg_type
+  constr with_bindings delayed_open) genarg_type
 
 val wit_bindings :
   (constr_expr bindings,
   glob_constr_and_expr bindings,
-  constr bindings Evd.sigma) genarg_type
+  constr bindings delayed_open) genarg_type
 
 val wit_hyp_location_flag : Locus.hyp_location_flag uniform_genarg_type
 
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 045beb37cf..cba10ca09d 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -55,7 +55,9 @@ let pr_with_bindings_typed prc prlc (c,bl) =
 let pr_fun_ind_using_typed prc prlc _ opt_c =
   match opt_c with
     | None -> mt ()
-    | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b.Evd.it)
+    | Some b ->
+      let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in
+      spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b)
 
 
 ARGUMENT EXTEND fun_ind_using
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index ff83ac3e9e..b98738ce31 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1433,7 +1433,7 @@ let () =
   Genprint.register_print0 Constrarg.wit_bindings
     (pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
     (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun { Evd.it = it } -> pr_bindings_no_with pr_constr pr_lconstr it);
+    (fun it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it)));
   Genprint.register_print0 Constrarg.wit_constr_may_eval
     (pr_may_eval pr_constr_expr pr_lconstr_expr (pr_or_by_notation pr_reference) pr_constr_pattern_expr)
     (pr_may_eval (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)
@@ -1442,7 +1442,7 @@ let () =
   Genprint.register_print0 Constrarg.wit_constr_with_bindings
     (pr_with_bindings pr_constr_expr pr_lconstr_expr)
     (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun { Evd.it = it } -> pr_with_bindings pr_constr pr_lconstr it);
+    (fun it -> pr_with_bindings pr_constr pr_lconstr (fst (run_delayed it)));
   Genprint.register_print0 Stdarg.wit_int int int int;
   Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool;
   Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit;
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 2682ca0708..10de3e866a 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -74,15 +74,13 @@ END
 
 TACTIC EXTEND left_with
   [ "left" "with" bindings(bl) ] -> [
-    let { Evd.sigma = sigma ; it = bl } = bl in
-    Tacticals.New.tclWITHHOLES false (Tactics.left_with_bindings false bl) sigma
+    Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.left_with_bindings false bl)
   ]
 END
 
 TACTIC EXTEND eleft_with
   [ "eleft" "with" bindings(bl) ] -> [
-    let { Evd.sigma = sigma ; it = bl } = bl in
-    Tacticals.New.tclWITHHOLES true (Tactics.left_with_bindings true bl) sigma
+    Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.left_with_bindings true bl)
   ]
 END
 
@@ -98,15 +96,13 @@ END
 
 TACTIC EXTEND right_with
   [ "right" "with" bindings(bl) ] -> [
-    let { Evd.sigma = sigma ; it = bl } = bl in
-    Tacticals.New.tclWITHHOLES false (Tactics.right_with_bindings false bl) sigma
+    Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.right_with_bindings false bl)
   ]
 END
 
 TACTIC EXTEND eright_with
   [ "eright" "with" bindings(bl) ] -> [
-    let { Evd.sigma = sigma ; it = bl } = bl in
-    Tacticals.New.tclWITHHOLES true (Tactics.right_with_bindings true bl) sigma
+    Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.right_with_bindings true bl)
   ]
 END
 
@@ -118,9 +114,8 @@ TACTIC EXTEND constructor
     Tactics.constructor_tac false None i NoBindings
   ]
 | [ "constructor" int_or_var(i) "with" bindings(bl) ] -> [
-    let { Evd.sigma = sigma; it = bl } = bl in
-    let tac = Tactics.constructor_tac false None i bl in
-    Tacticals.New.tclWITHHOLES false tac sigma
+    let tac bl = Tactics.constructor_tac false None i bl in
+    Tacticals.New.tclDELAYEDWITHHOLES false bl tac
   ]
 END
 
@@ -130,9 +125,8 @@ TACTIC EXTEND econstructor
     Tactics.constructor_tac true None i NoBindings
   ]
 | [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> [
-    let { Evd.sigma = sigma; it = bl } = bl in
-    let tac = Tactics.constructor_tac true None i bl in
-    Tacticals.New.tclWITHHOLES true tac sigma
+    let tac bl = Tactics.constructor_tac true None i bl in
+    Tacticals.New.tclDELAYEDWITHHOLES true bl tac
   ]
 END
 
@@ -140,8 +134,7 @@ END
 
 TACTIC EXTEND specialize
   [ "specialize" constr_with_bindings(c) ] -> [
-    let { Evd.sigma = sigma; it = c } = c in
-    Tacticals.New.tclWITHHOLES false (Tactics.specialize c) sigma
+    Tacticals.New.tclDELAYEDWITHHOLES false c Tactics.specialize
   ]
 END
 
@@ -161,15 +154,13 @@ END
 
 TACTIC EXTEND split_with
   [ "split" "with" bindings(bl) ] -> [
-    let { Evd.sigma = sigma ; it = bl } = bl in
-    Tacticals.New.tclWITHHOLES false (Tactics.split_with_bindings false [bl]) sigma
+    Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.split_with_bindings false [bl])
   ]
 END
 
 TACTIC EXTEND esplit_with
   [ "esplit" "with" bindings(bl) ] -> [
-    let { Evd.sigma = sigma ; it = bl } = bl in
-    Tacticals.New.tclWITHHOLES true (Tactics.split_with_bindings true [bl]) sigma
+    Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.split_with_bindings true [bl])
   ]
 END
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 4ddf9c1162..dce7a18608 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -70,8 +70,8 @@ let induction_arg_of_quantified_hyp = function
    ElimOnIdent and not as "constr" *)
 
 let elimOnConstrWithHoles tac with_evars c =
-  Tacticals.New.tclWITHHOLES with_evars
-    (tac with_evars (Some (None,ElimOnConstr c.it))) c.sigma
+  Tacticals.New.tclDELAYEDWITHHOLES with_evars c
+    (fun c -> tac with_evars (Some (None,ElimOnConstr c)))
 
 TACTIC EXTEND simplify_eq_main
 | [ "simplify_eq" constr_with_bindings(c) ] ->
@@ -116,7 +116,7 @@ END
 open Proofview.Notations
 let discrHyp id =
   Proofview.tclEVARMAP >>= fun sigma ->
-  discr_main {it = Term.mkVar id,NoBindings; sigma = sigma;}
+  discr_main { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma }
 
 let injection_main c =
  elimOnConstrWithHoles (injClause None) false c
@@ -161,7 +161,7 @@ END
 
 let injHyp id =
   Proofview.tclEVARMAP >>= fun sigma ->
-  injection_main { it = Term.mkVar id,NoBindings; sigma = sigma; }
+  injection_main { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma }
 
 TACTIC EXTEND dependent_rewrite
 | [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
@@ -201,7 +201,7 @@ END
 
 let onSomeWithHoles tac = function
   | None -> tac None
-  | Some c -> Tacticals.New.tclWITHHOLES false (tac (Some c.it)) c.sigma
+  | Some c -> Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> tac (Some c))
 
 TACTIC EXTEND contradiction
  [ "contradiction" constr_with_bindings_opt(c) ] ->
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 72c2679c06..1d2e497d51 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -11,4 +11,4 @@ val injHyp : Names.Id.t -> unit Proofview.tactic
 
 (* val refine_tac : Evd.open_constr -> unit Proofview.tactic *)
 
-val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Evd.sigma option -> unit Proofview.tactic
+val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Tacexpr.delayed_open option -> unit Proofview.tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d96c8f98a2..16cafafeb8 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2277,13 +2277,15 @@ let () =
 let lift f = (); fun ist gl x -> (project gl, f ist (pf_env gl) (project gl) x)
 let lifts f = (); fun ist gl x -> f ist (pf_env gl) (project gl) x
 
-let interp_bindings' ist gl bl =
-  let (sigma, bl) = interp_bindings ist (pf_env gl) (project gl) bl in
-  (project gl, pack_sigma (sigma, bl))
-
-let interp_constr_with_bindings' ist gl c =
-  let (sigma, c) = interp_constr_with_bindings ist (pf_env gl) (project gl) c in
-  (project gl, pack_sigma (sigma, c))
+let interp_bindings' ist gl bl = (project gl, { delayed = fun env sigma ->
+  let (sigma, bl) = interp_bindings ist env (Sigma.to_evar_map sigma) bl in
+  Sigma.Unsafe.of_pair (bl, sigma)
+  })
+
+let interp_constr_with_bindings' ist gl c = (project gl, { delayed = fun env sigma ->
+  let (sigma, c) = interp_constr_with_bindings ist env (Sigma.to_evar_map sigma) c in
+  Sigma.Unsafe.of_pair (c, sigma)
+  })
 
 let () =
   Geninterp.register_interp0 wit_int_or_var (fun ist gl n -> project gl, interp_int_or_var ist n);
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index e181c8e14e..74714300c4 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -515,6 +515,14 @@ module New = struct
         in
         Proofview.Unsafe.tclEVARS sigma <*> tac >>= check_evars_if
 
+  let tclDELAYEDWITHHOLES check x tac =
+    Proofview.Goal.nf_enter { enter = begin fun gl ->
+      let env = Proofview.Goal.env gl in
+      let sigma = Proofview.Goal.sigma gl in
+      let Sigma (x, sigma, _) = x.Tacexpr.delayed env sigma in
+      tclWITHHOLES check (tac x) (Sigma.to_evar_map sigma)
+    end }
+
   let tclTIMEOUT n t =
     Proofview.tclOR
       (Proofview.tclTIMEOUT n t)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 80e01a8d07..042f80fe82 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -219,6 +219,7 @@ module New : sig
   val tclSOLVE : unit tactic list -> unit tactic
   val tclPROGRESS : unit tactic -> unit tactic
   val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
+  val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic
 
   val tclTIMEOUT : int -> unit tactic -> unit tactic
   val tclTIME : string option -> 'a tactic -> 'a tactic