Type delayed_open_constr is now monotonic.

8 files changed, 56 insertions, 27 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 45f482cd44..124d4c0fef 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -122,11 +122,12 @@ type open_glob_constr = unit * glob_constr_and_expr
 type binding_bound_vars = Id.Set.t
 type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
 
-type delayed_open_constr_with_bindings =
-    Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr with_bindings
+type 'a delayed_open =
+  { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
 
-type delayed_open_constr =
-    Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr
+type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open
+
+type delayed_open_constr = Term.constr delayed_open
 
 type intro_pattern = delayed_open_constr intro_pattern_expr located
 type intro_patterns = delayed_open_constr intro_pattern_expr located list
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index eadeebd38e..ab3629f89e 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -10,6 +10,7 @@ open Glob_term
 open Declarations
 open Misctypes
 open Decl_kinds
+open Sigma.Notations
 
 let is_rec_info scheme_info =
   let test_branche min acc (_,_,br) =
@@ -86,7 +87,7 @@ let functional_induction with_clean c princl pat =
       in
       let encoded_pat_as_patlist =
         List.make (List.length args + List.length c_list - 1) None @ [pat] in
-      List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr (fun env sigma -> sigma,(c,NoBindings))),(None,pat),None))
+      List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) })),(None,pat),None))
         (args@c_list) encoded_pat_as_patlist
     in
     let princ' = Some (princ,bindings) in
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index e8ccd29c8a..72d2eedcc3 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1437,6 +1437,9 @@ end)
 
 (** Registering *)
 
+let run_delayed c =
+  Sigma.run Evd.empty { Sigma.run = fun sigma -> c.delayed (Global.env ()) sigma }
+
 let () =
   let pr_bool b = if b then str "true" else str "false" in
   let pr_unit _ = str "()" in
@@ -1447,7 +1450,7 @@ let () =
     Constrarg.wit_intro_pattern
     (Miscprint.pr_intro_pattern pr_constr_expr)
     (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
-    (Miscprint.pr_intro_pattern (fun c -> pr_constr (snd (c (Global.env()) Evd.empty))));
+    (Miscprint.pr_intro_pattern (fun c -> pr_constr (fst (run_delayed c))));
   Genprint.register_print0
     Constrarg.wit_clause_dft_concl
     (pr_clauses (Some true) pr_lident)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 1f66699004..c6d74525fe 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -487,7 +487,7 @@ let apply_special_clear_request clear_flag f =
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     try
-      let sigma,(c,bl) = f env sigma in
+      let ((c, bl), sigma) = run_delayed env sigma f in
       apply_clear_request clear_flag (use_clear_hyp_by_default ()) c
     with
       e when catchable_exception e -> tclIDTAC
@@ -498,7 +498,7 @@ let general_multi_rewrite with_evars l cl tac =
     Proofview.Goal.enter begin fun gl ->
       let sigma = Proofview.Goal.sigma gl in
       let env = Proofview.Goal.env gl in
-      let sigma,c = f env sigma in
+      let (c, sigma) = run_delayed env sigma f in
       tclWITHHOLES with_evars
         (general_rewrite_clause l2r with_evars ?tac c cl) sigma
     end
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 85f2d2f91f..d3d5c9a9bd 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -285,10 +285,10 @@ let error_too_many_names pats =
   tclZEROMSG ~loc (
     str "Unexpected " ++
     str (String.plural (List.length pats) "introduction pattern") ++
-    str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (snd (c env Evd.empty)))) pats ++
+    str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (fst (run_delayed env Evd.empty c)))) pats ++
     str ".")
 
-let rec get_names (allow_conj,issimple) (loc,pat as x) = match pat with
+let get_names (allow_conj,issimple) (loc, pat as x) = match pat with
   | IntroNaming IntroAnonymous | IntroForthcoming _ ->
       error "Anonymous pattern not allowed for inversion equations."
   | IntroNaming (IntroFresh _) ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 96d0b592b8..ec6f041336 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -40,6 +40,7 @@ open Misctypes
 open Locus
 open Tacintern
 open Taccoerce
+open Sigma.Notations
 open Proofview.Notations
 
 let safe_msgnl s =
@@ -801,7 +802,7 @@ let rec message_of_value v =
     Ftactic.return (int (out_gen (topwit wit_int) v))
   else if has_type v (topwit wit_intro_pattern) then
     let p = out_gen (topwit wit_intro_pattern) v in
-    let print env sigma c = pr_constr_env env sigma (snd (c env Evd.empty)) in
+    let print env sigma c = pr_constr_env env sigma (fst (Tactics.run_delayed env Evd.empty c)) in
     Ftactic.nf_enter begin fun gl ->
       Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (Proofview.Goal.sigma gl) c) p)
     end
@@ -864,7 +865,11 @@ and interp_intro_pattern_action ist env sigma = function
       let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in
       sigma, IntroInjection l
   | IntroApplyOn (c,ipat) ->
-      let c = fun env sigma -> interp_constr ist env sigma c in
+      let c = { delayed = fun env sigma ->
+        let sigma = Sigma.to_evar_map sigma in
+        let (sigma, c) = interp_constr ist env sigma c in
+        Sigma.Unsafe.of_pair (c, sigma)
+      } in
       let sigma,ipat = interp_intro_pattern ist env sigma ipat in
       sigma, IntroApplyOn (c,ipat)
   | IntroWildcard | IntroRewrite _ as x -> sigma, x
@@ -967,13 +972,21 @@ let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) =
   let loc1 = loc_of_glob_constr c in
   let loc2 = loc_of_bindings bl in
   let loc = if Loc.is_ghost loc2 then loc1 else Loc.merge loc1 loc2 in
-  let f env sigma = interp_open_constr_with_bindings ist env sigma cb in
+  let f = { delayed = fun env sigma ->
+    let sigma = Sigma.to_evar_map sigma in
+    let (sigma, c) = interp_open_constr_with_bindings ist env sigma cb in
+    Sigma.Unsafe.of_pair (c, sigma)
+  } in
     (loc,f)
 
 let interp_induction_arg ist gl arg =
   match arg with
   | keep,ElimOnConstr c ->
-      keep,ElimOnConstr (fun env sigma -> interp_constr_with_bindings ist env sigma c)
+      keep,ElimOnConstr { delayed = fun env sigma ->
+        let sigma = Sigma.to_evar_map sigma in
+        let (sigma, c) = interp_constr_with_bindings ist env sigma c in
+        Sigma.Unsafe.of_pair (c, sigma)
+      }
   | keep,ElimOnAnonHyp n as x -> x
   | keep,ElimOnIdent (loc,id) ->
       let error () = user_err_loc (loc, "",
@@ -984,7 +997,7 @@ let interp_induction_arg ist gl arg =
         if Tactics.is_quantified_hypothesis id' gl
         then keep,ElimOnIdent (loc,id')
         else
-          (try keep,ElimOnConstr (fun env sigma -> sigma,(constr_of_id env id',NoBindings))
+          (try keep,ElimOnConstr { delayed = fun env sigma -> Sigma ((constr_of_id env id',NoBindings), sigma, Sigma.refl) }
           with Not_found ->
             user_err_loc (loc,"",
             pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis."))
@@ -1005,16 +1018,18 @@ let interp_induction_arg ist gl arg =
           keep,ElimOnAnonHyp (out_gen (topwit wit_int) v)
         else match Value.to_constr v with
         | None -> error ()
-        | Some c -> keep,ElimOnConstr (fun env sigma -> sigma,(c,NoBindings))
+        | Some c -> keep,ElimOnConstr { delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) }
       with Not_found ->
 	(* We were in non strict (interactive) mode *)
 	if Tactics.is_quantified_hypothesis id gl then
           keep,ElimOnIdent (loc,id)
 	else
           let c = (GVar (loc,id),Some (CRef (Ident (loc,id),None))) in
-          let f env sigma = 
+          let f = { delayed = fun env sigma ->
+            let sigma = Sigma.to_evar_map sigma in
             let (sigma,c) = interp_open_constr ist env sigma c in
-            sigma,(c,NoBindings) in
+            Sigma.Unsafe.of_pair ((c,NoBindings), sigma)
+          } in
           keep,ElimOnConstr f
 
 (* Associates variables with values and gives the remaining variables and
@@ -2185,7 +2200,11 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacRewrite (ev,l,cl,by) ->
       Proofview.Goal.enter begin fun gl ->
         let l' = List.map (fun (b,m,(keep,c)) ->
-          let f env sigma = interp_open_constr_with_bindings ist env sigma c in
+          let f = { delayed = fun env sigma ->
+            let sigma = Sigma.to_evar_map sigma in
+            let (sigma, c) = interp_open_constr_with_bindings ist env sigma c in
+            Sigma.Unsafe.of_pair (c, sigma)
+          } in
 	  (b,m,keep,f)) l in
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8cc460560b..04ee0183a0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -981,12 +981,15 @@ let rec intros_move = function
       Tacticals.New.tclTHEN (intro_gen (NamingMustBe (dloc,hyp)) destopt false false)
 	(intros_move rest)
 
+let run_delayed env sigma c =
+  Sigma.run sigma { Sigma.run = fun sigma -> c.delayed env sigma }
+
 (* Apply a tactic on a quantified hypothesis, an hypothesis in context
    or a term with bindings *)
 
 let onOpenInductionArg env sigma tac = function
   | clear_flag,ElimOnConstr f ->
-      let (sigma',cbl) = f env sigma in
+      let (cbl, sigma') = run_delayed env sigma f in
       let pending = (sigma,sigma') in
       Tacticals.New.tclTHEN
         (Proofview.Unsafe.tclEVARS sigma')
@@ -1578,7 +1581,7 @@ let apply_with_delayed_bindings_gen b e l =
     Proofview.Goal.enter begin fun gl ->
       let sigma = Proofview.Goal.sigma gl in
       let env = Proofview.Goal.env gl in
-      let sigma, cb = f env sigma in
+      let (cb, sigma) = run_delayed env sigma f in
 	Tacticals.New.tclWITHHOLES e
           (general_apply b b e k (loc,cb)) sigma
     end
@@ -1680,7 +1683,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
-    let sigma, c = f env sigma in
+    let (c, sigma) = run_delayed env sigma f in
     Tacticals.New.tclWITHHOLES with_evars 
       (apply_in_once sidecond_first with_delta with_destruct with_evars
          naming id (clear_flag,(loc,c)) tac)
@@ -2245,7 +2248,7 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with
       Proofview.Goal.enter begin fun gl ->
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
-        let sigma,c = f env sigma in
+        let (c, sigma) = run_delayed env sigma f in
         Tacticals.New.tclWITHHOLES false
           (Tacticals.New.tclTHENFIRST
              (* Skip the side conditions of the apply *)
@@ -2339,7 +2342,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
 *)
 
 let apply_in simple with_evars clear_flag id lemmas ipat =
-  let lemmas = List.map (fun (k,(loc,l)) -> k, (loc, fun _ sigma -> sigma, l)) lemmas in
+  let lemmas = List.map (fun (k,(loc,l)) -> k, (loc, { delayed = fun _ sigma -> Sigma (l, sigma, Sigma.refl) })) lemmas in
   general_apply_in false simple simple with_evars clear_flag id lemmas ipat
 
 let apply_delayed_in simple with_evars clear_flag id lemmas ipat =
@@ -2729,7 +2732,7 @@ let check_unused_names names =
       (str"Unused introduction " ++ str (String.plural (List.length names) "pattern")
        ++ str": " ++ prlist_with_sep spc 
 	 (Miscprint.pr_intro_pattern 
-	    (fun c -> Printer.pr_constr (snd (c (Global.env()) Evd.empty)))) names)
+	    (fun c -> Printer.pr_constr (fst (run_delayed (Global.env()) Evd.empty c)))) names)
 
 let intropattern_of_name gl avoid = function
   | Anonymous -> IntroNaming IntroAnonymous
@@ -4118,7 +4121,7 @@ let induction_destruct isrec with_evars (lc,elim) =
       (* will be removable when is_functional_induction will be more clever *)
       if not (Option.is_empty cls) then error "'in' clause not supported here.";
       let finish_evar_resolution f =
-        let (sigma',(c,lbind)) = f env sigma in
+        let ((c, lbind), sigma') = run_delayed env sigma f in
         let pending = (sigma,sigma') in
         let sigma' = Sigma.Unsafe.of_evar_map sigma' in
         let Sigma (c, _, _) = finish_evar_resolution env sigma' (pending,c) in
@@ -4161,7 +4164,7 @@ let induction_destruct isrec with_evars (lc,elim) =
     | Some elim ->
       (* Several induction hyps with induction scheme *)
       let finish_evar_resolution f =
-        let (sigma',(c,lbind)) = f env sigma in
+        let ((c, lbind), sigma') = run_delayed env sigma f in
         let pending = (sigma,sigma') in
 	if lbind != NoBindings then
 	  error "'with' clause not supported here.";
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 38e6ce0eaf..d62d27ca34 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -205,6 +205,8 @@ val apply_delayed_in :
     (clear_flag * delayed_open_constr_with_bindings located) list ->
     intro_pattern option -> unit Proofview.tactic
 
+val run_delayed : Environ.env -> evar_map -> 'a delayed_open -> 'a * evar_map
+
 (** {6 Elimination tactics. } *)
 
 (*