Remove the Sigma (monotonous state) API.

Reminder of (some of) the reasons for removal:

- Despite the claim in sigma.mli, it does *not* prevent evar
  leaks, something like:

  fun env evd ->
  let (evd',ev) = new_evar env evd in
  (evd,ev)

  will typecheck even with Sigma-like type annotations (with a proof of
  reflexivity)

- The API stayed embryonic. Even typing functions were not ported to
  Sigma.

- Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly
  less unsafe ones (e.g. s_enter), but those ones were not marked unsafe
  at all (despite still being so).

- There was no good story for higher order functions manipulating evar
  maps. Without higher order, one can most of the time get away with
  reusing the same name for the updated evar map.

- Most of the code doing complex things with evar maps was using unsafe
  casts to sigma. This code should be fixed, but this is an orthogonal
  issue.

Of course, this was showing a nice and elegant use of GADTs, but the
cost/benefit ratio in practice did not seem good.

1 files changed, 34 insertions, 37 deletions

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 0cd18ae50..465e77019 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -28,7 +28,6 @@ open Globnames
 open Nametab
 open Contradiction
 open Misctypes
-open Proofview.Notations
 open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
@@ -38,12 +37,12 @@ open OmegaSolver
 (* Added by JCF, 09/03/98 *)
 
 let elim_id id =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     simplest_elim (mkVar id)
-  end }
-let resolve_id id = Proofview.Goal.enter { enter = begin fun gl ->
+  end
+let resolve_id id = Proofview.Goal.enter begin fun gl ->
   apply (mkVar id)
-end }
+end
 
 let timing timer_name f arg = f arg
 
@@ -580,10 +579,10 @@ let abstract_path sigma typ path t =
 
 let focused_simpl path =
   let open Tacmach.New in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.nf_enter begin fun gl ->
   let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
   convert_concl_no_check newc DEFAULTcast
-  end }
+  end
 
 let focused_simpl path = focused_simpl path
 
@@ -643,17 +642,16 @@ let decompile af =
 
 (** Backward compat to emulate the old Refine: normalize the goal conclusion *)
 let new_hole env sigma c =
-  let c = Reductionops.nf_betaiota (Sigma.to_evar_map sigma) c in
+  let c = Reductionops.nf_betaiota sigma c in
   Evarutil.new_evar env sigma c
 
 let clever_rewrite_base_poly typ p result theorem =
   let open Tacmach.New in
-  let open Sigma in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.nf_enter begin fun gl ->
   let full = pf_concl gl in
   let env = pf_env gl in
   let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in
-  Refine.refine { run = begin fun sigma ->
+  Refine.refine begin fun sigma ->
   let t =
     applist
       (mkLambda
@@ -667,10 +665,10 @@ let clever_rewrite_base_poly typ p result theorem =
        [abstracted])
   in
   let argt = mkApp (abstracted, [|result|]) in
-  let Sigma (hole, sigma, p) = new_hole env sigma argt in
-  Sigma (applist (t, [hole]), sigma, p)
-  end }
-  end }
+  let (sigma, hole) = new_hole env sigma argt in
+  (sigma, applist (t, [hole]))
+  end
+  end
 
 let clever_rewrite_base p result theorem =
   clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem
@@ -689,26 +687,25 @@ let clever_rewrite_gen_nat p result (t,args) =
 (** Solve using the term the term [t _] *)
 let refine_app gl t =
   let open Tacmach.New in
-  let open Sigma in
-  Refine.refine { run = begin fun sigma ->
+  Refine.refine begin fun sigma ->
   let env = pf_env gl in
-  let ht = match EConstr.kind (Sigma.to_evar_map sigma) (pf_get_type_of gl t) with
+  let ht = match EConstr.kind sigma (pf_get_type_of gl t) with
   | Prod (_, t, _) -> t
   | _ -> assert false
   in
-  let Sigma (hole, sigma, p) = new_hole env sigma ht in
-  Sigma (applist (t, [hole]), sigma, p)
-  end }
+  let (sigma, hole) = new_hole env sigma ht in
+  (sigma, applist (t, [hole]))
+  end
 
 let clever_rewrite p vpath t =
   let open Tacmach.New in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.nf_enter begin fun gl ->
   let full = pf_concl gl in
   let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in
   let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in
   let t' = applist(t, (vargs @ [abstracted])) in
   refine_app gl t'
-  end }
+  end
 
 let rec shuffle p (t1,t2) =
   match t1,t2 with
@@ -1466,7 +1463,7 @@ let reintroduce id =
 open Proofview.Notations
 
 let coq_omega =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   clear_constr_tables ();
   let hyps_types = Tacmach.New.pf_hyps_types gl in
   let destructure_omega = destructure_omega gl in
@@ -1514,12 +1511,12 @@ let coq_omega =
       tclTHEN prelude (replay_history tactic_normalisation path)
     with NO_CONTRADICTION -> tclZEROMSG (Pp.str"Omega can't solve this system")
   end
-  end }
+  end
 
 let coq_omega = coq_omega
 
 let nat_inject =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in
   let rec explore p t : unit Proofview.tactic =
     Proofview.tclEVARMAP >>= fun sigma ->
@@ -1655,7 +1652,7 @@ let nat_inject =
   in
   let hyps_types = Tacmach.New.pf_hyps_types gl in
   loop (List.rev hyps_types)
-  end }
+  end
 
 let dec_binop = function
   | Zne -> coq_dec_Zne
@@ -1729,19 +1726,19 @@ let onClearedName id tac =
   (* so renaming may be necessary *)
   tclTHEN
     (tclTRY (clear [id]))
-    (Proofview.Goal.nf_enter { enter = begin fun gl ->
+    (Proofview.Goal.nf_enter begin fun gl ->
      let id = fresh_id [] id gl in
      tclTHEN (introduction id) (tac id)
-    end })
+    end)
 
 let onClearedName2 id tac =
   tclTHEN
     (tclTRY (clear [id]))
-    (Proofview.Goal.nf_enter { enter = begin fun gl ->
+    (Proofview.Goal.nf_enter begin fun gl ->
      let id1 = fresh_id [] (add_suffix id "_left") gl in
      let id2 = fresh_id [] (add_suffix id "_right") gl in
       tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
-    end })
+    end)
 
 let rec is_Prop sigma c = match EConstr.kind sigma c with
   | Sort s -> Sorts.is_prop (ESorts.kind sigma s)
@@ -1749,7 +1746,7 @@ let rec is_Prop sigma c = match EConstr.kind sigma c with
   | _ -> false
 
 let destructure_hyps =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let type_of = Tacmach.New.pf_unsafe_type_of gl in
   let decidability = decidability gl in
   let pf_nf = pf_nf gl in
@@ -1888,10 +1885,10 @@ let destructure_hyps =
     in
     let hyps = Proofview.Goal.hyps gl in
     loop hyps
-  end }
+  end
 
 let destructure_goal =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let decidability = decidability gl in
     let rec loop t =
@@ -1910,9 +1907,9 @@ let destructure_goal =
 	    try
 	      let dec = decidability t in
 	      tclTHEN
-                (Proofview.Goal.nf_enter { enter = begin fun gl ->
+                (Proofview.Goal.nf_enter begin fun gl ->
 		                         refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |]))
-		                         end })
+		                         end)
 	        intro
 	    with Undecidable -> Tactics.elim_type (Lazy.force coq_False)
 	    | e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
@@ -1920,7 +1917,7 @@ let destructure_goal =
 	  tclTHEN goal_tac destructure_hyps
     in
     (loop concl)
-  end }
+  end
 
 let destructure_goal = destructure_goal