Merge PR#623: Remove the Sigma (monotonous state) API.

5 files changed, 9 insertions, 15 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index c2f705898f..fd49623986 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1481,7 +1481,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 			    tclCOMPLETE(
 				    Eauto.eauto_with_bases
 				      (true,5)
-				      [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}]
+				      [(fun _ sigma -> (sigma, Lazy.force refl_equal))]
 				      [Hints.Hint_db.empty empty_transparent_state false]
 				  )
 			   )
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index a0eb9e2b27..b8070ff885 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -12,7 +12,6 @@ open Context.Rel.Declaration
 open Indfun_common
 open Functional_principles_proofs
 open Misctypes
-open Sigma.Notations
 
 module RelDecl = Context.Rel.Declaration
 
@@ -669,11 +668,9 @@ let build_case_scheme fa =
 	 let ind = first_fun_kn,funs_indexes in
 	   (ind,Univ.Instance.empty)(*FIXME*),prop_sort
   in
-  let sigma = Sigma.Unsafe.of_evar_map sigma in
-  let Sigma (scheme, sigma, _) = 
+  let (sigma, scheme) = 
       Indrec.build_case_analysis_scheme_default env sigma ind sf
   in
-  let sigma = Sigma.to_evar_map sigma in
   let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in
   let sorts =
     (fun (_,_,x) ->
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index bd2ac8c67b..d28e0aba0a 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -37,9 +37,10 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
   match opt_c with
     | None -> mt ()
     | Some b ->
-      let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in
+      let (_, b) = b (Global.env ()) Evd.empty in
       spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
 
+
 ARGUMENT EXTEND fun_ind_using
   TYPED AS constr_with_bindings option
   PRINTED BY pr_fun_ind_using_typed
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index a23c51495c..f1a9758e80 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -11,7 +11,6 @@ open Glob_term
 open Declarations
 open Misctypes
 open Decl_kinds
-open Sigma.Notations
 
 module RelDecl = Context.Rel.Declaration
 
@@ -93,7 +92,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 ({ Tacexpr.delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) })),(None,pat),None))
+      List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)) )),(None,pat),None))
         (args@c_list) encoded_pat_as_patlist
     in
     let princ' = Some (princ,bindings) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index e6f199dbae..ff397d2e92 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -42,7 +42,6 @@ open Auto
 open Eauto
 
 open Indfun_common
-open Sigma.Notations
 open Context.Rel.Declaration
 
 (* Ugly things which should not be here *)
@@ -700,11 +699,9 @@ let mkDestructEq :
     observe_tclTHENLIST (str "mkDestructEq")
      [Proofview.V82.of_tactic (generalize new_hyps);
       (fun g2 ->
-        let changefun patvars = { run = fun sigma ->
-          let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in
-          let Sigma (c, sigma, p) = redfun.Reductionops.e_redfun (pf_env g2) sigma (pf_concl g2) in
-          Sigma (c, sigma, p)
-        } in
+        let changefun patvars sigma =
+          pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2)
+        in
 	Proofview.V82.of_tactic (change_in_concl None changefun) g2);
       Proofview.V82.of_tactic (simplest_case expr)]), to_revert
 
@@ -1357,7 +1354,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 			  (Proofview.V82.of_tactic e_assumption);
 		      Eauto.eauto_with_bases
 			(true,5)
-			[{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}]
+			[(fun _ sigma -> (sigma, (Lazy.force refl_equal)))]
 			[Hints.Hint_db.empty empty_transparent_state false]
 		      ]
 		    )