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.

4 files changed, 40 insertions, 44 deletions

diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index bbb9feae2..e3fab6d01 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -15,7 +15,6 @@ open Ground
 open Goptions
 open Tacmach.New
 open Tacticals.New
-open Proofview.Notations
 open Tacinterp
 open Libnames
 open Stdarg
@@ -84,24 +83,24 @@ let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
 let gen_ground_tac flag taco ids bases =
   let backup= !qflag in
   Proofview.tclOR begin
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
       qflag:=flag;
       let solver=
 	match taco with
 	    Some tac-> tac
 	  | None-> snd (default_solver ()) in
       let startseq k =
-        Proofview.Goal.s_enter { s_enter = begin fun gl ->
+        Proofview.Goal.enter begin fun gl ->
 	let seq=empty_seq !ground_depth in
         let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in
         let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in
-        Sigma.Unsafe.of_pair (k seq, sigma)
-        end }
+        tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq)
+        end
       in
       let result=ground_tac solver startseq in
       qflag := backup;
       result
-  end }
+  end
   end
   (fun (e, info) -> qflag := backup; Proofview.tclZERO ~info e)
 
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index ab1dd07c1..0fa3089e7 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -14,7 +14,6 @@ open Instances
 open Term
 open Tacmach.New
 open Tacticals.New
-open Proofview.Notations
 
 let update_flags ()=
   let predref=ref Names.Cpred.empty in
@@ -31,10 +30,10 @@ let update_flags ()=
       (Names.Id.Pred.full,Names.Cpred.complement !predref)
 
 let ground_tac solver startseq =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   update_flags ();
   let rec toptac skipped seq =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let () =
       if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
       then
@@ -127,7 +126,7 @@ let ground_tac solver startseq =
 		  end
 	    with Heap.EmptyHeap->solver
       end
-    end } in
+    end in
     let n = List.length (Proofview.Goal.hyps gl) in
     startseq (fun seq -> wrap n true (toptac []) seq)
-  end }
+  end
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 04bca584f..e1d765a42 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -21,7 +21,6 @@ open Formula
 open Sequent
 open Names
 open Misctypes
-open Sigma.Notations
 open Context.Rel.Declaration
 
 let compare_instance inst1 inst2=
@@ -114,9 +113,7 @@ let mk_open_instance env evmap id idc m t =
   let rec aux n avoid env evmap decls =
     if Int.equal n 0 then evmap, decls else
       let nid=(fresh_id_in_env avoid var_id env) in
-      let evmap = Sigma.Unsafe.of_evar_map evmap in
-      let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
-      let evmap = Sigma.to_evar_map evmap in
+      let (evmap, (c, _)) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
       let decl = LocalAssum (Name nid, c) in
 	aux (n-1) (nid::avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
   let evmap, decls = aux m [] env evmap [] in
@@ -126,7 +123,7 @@ let mk_open_instance env evmap id idc m t =
 
 let left_instance_tac (inst,id) continue seq=
   let open EConstr in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let sigma = project gl in
   match inst with
       Phantom dom->
@@ -137,10 +134,10 @@ let left_instance_tac (inst,id) continue seq=
 	    [tclTHENLIST
 	       [introf;
                 (pf_constr_of_global id >>= fun idc ->
-                Proofview.Goal.enter { enter = begin fun gl ->
+                Proofview.Goal.enter begin fun gl ->
                   let id0 = List.nth (pf_ids_of_hyps gl) 0 in
                   generalize [mkApp(idc, [|mkVar id0|])]
-                end });
+                end);
 		introf;
 		tclSOLVE [wrap 1 false continue
 			    (deepen (record (id,None) seq))]];
@@ -153,7 +150,7 @@ let left_instance_tac (inst,id) continue seq=
 	  let special_generalize=
 	    if m>0 then
 	      (pf_constr_of_global id >>= fun idc ->
-		Proofview.Goal.s_enter { s_enter = begin fun gl->
+		Proofview.Goal.enter begin fun gl->
 		  let (evmap, rc, ot) = mk_open_instance (pf_env gl) (project gl) id idc m t in
 		  let gt=
 		    it_mkLambda_or_LetIn
@@ -162,8 +159,9 @@ let left_instance_tac (inst,id) continue seq=
 		    try Typing.type_of (pf_env gl) evmap gt
 		    with e when CErrors.noncritical e ->
 		      user_err Pp.(str "Untypable instance, maybe higher-order non-prenex quantification") in
-		    Sigma.Unsafe.of_pair (generalize [gt], evmap)
-                end })
+                  Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evmap)
+		    (generalize [gt])
+                end)
 	    else
 	      pf_constr_of_global id >>= fun idc -> generalize [mkApp(idc,[|t|])]
 	  in
@@ -172,20 +170,20 @@ let left_instance_tac (inst,id) continue seq=
 	       introf;
 	       tclSOLVE
 		 [wrap 1 false continue (deepen (record (id,Some c) seq))]]
-  end }
+  end
 
 let right_instance_tac inst continue seq=
   let open EConstr in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   match inst with
       Phantom dom ->
 	tclTHENS (cut dom)
 	[tclTHENLIST
 	   [introf;
-            Proofview.Goal.enter { enter = begin fun gl ->
+            Proofview.Goal.enter begin fun gl ->
               let id0 = List.nth (pf_ids_of_hyps gl) 0 in
               split (ImplicitBindings [mkVar id0])
-            end };
+            end;
 	    tclSOLVE [wrap 0 true continue (deepen seq)]];
 	 tclTRY assumption]
     | Real ((0,t),_) ->
@@ -193,7 +191,7 @@ let right_instance_tac inst continue seq=
 	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
     | Real ((m,t),_) ->
 	tclFAIL 0 (Pp.str "not implemented ... yet")
-  end }
+  end
 
 let instance_tac inst=
   if (snd inst)==dummy_id then
@@ -202,9 +200,9 @@ let instance_tac inst=
     left_instance_tac inst
 
 let quantified_tac lf backtrack continue seq =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let insts=give_instances (project gl) lf seq in
     tclORELSE
       (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts))
       backtrack
-  end }
+  end
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index f745dbeb4..b7fe25a32 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -32,7 +32,7 @@ type lseqtac= global_reference -> seqtac
 type 'a with_backtracking = tactic -> 'a
 
 let wrap n b continue seq =
-  Proofview.Goal.nf_enter { enter = begin fun gls ->
+  Proofview.Goal.nf_enter begin fun gls ->
   Control.check_for_interrupt ();
   let nc = Proofview.Goal.hyps gls in
   let env=pf_env gls in
@@ -52,7 +52,7 @@ let wrap n b continue seq =
   let seq2=if b then
     add_formula env sigma Concl dummy_id (pf_concl gls) seq1 else seq1 in
     continue seq2
-  end }
+  end
 
 let basename_of_global=function
     VarRef id->id
@@ -65,12 +65,12 @@ let clear_global=function
 (* connection rules *)
 
 let axiom_tac t seq =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   try
     pf_constr_of_global (find_left (project gl) t seq) >>= fun c ->
     exact_no_check c
   with Not_found -> tclFAIL 0 (Pp.str "No axiom link")
-  end }
+  end
 
 let ll_atom_tac a backtrack id continue seq =
   let open EConstr in
@@ -107,7 +107,7 @@ let arrow_tac backtrack continue seq=
 (* left connectives rules *)
 
 let left_and_tac ind backtrack id continue seq =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let n=(construct_nhyps (pf_env gl) ind).(0) in
    tclIFTHENELSE
      (tclTHENLIST
@@ -116,10 +116,10 @@ let left_and_tac ind backtrack id continue seq =
        tclDO n intro])
      (wrap n false continue seq)
      backtrack
-  end }
+  end
 
 let left_or_tac ind backtrack id continue seq =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let v=construct_nhyps (pf_env gl) ind in
   let f n=
     tclTHENLIST
@@ -130,7 +130,7 @@ let left_or_tac ind backtrack id continue seq =
       (pf_constr_of_global id >>= simplest_elim)
       (Array.map f v)
       backtrack
-  end }
+  end
 
 let left_false_tac id=
   Tacticals.New.pf_constr_of_global id >>= simplest_elim
@@ -140,7 +140,7 @@ let left_false_tac id=
 (* We use this function for false, and, or, exists *)
 
 let ll_ind_tac (ind,u as indu) largs backtrack id continue seq =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
      let rcs=ind_hyps (pf_env gl) (project gl) 0 indu largs in
      let vargs=Array.of_list largs in
              (* construire le terme  H->B, le generaliser etc *)
@@ -161,7 +161,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq =
 	       clear_global id;
 	       tclDO lp intro])
 	   (wrap lp false continue seq) backtrack
-  end }
+  end
 
 let ll_arrow_tac a b c backtrack id continue seq=
   let open EConstr in
@@ -199,7 +199,7 @@ let forall_tac backtrack continue seq=
        backtrack)
 
 let left_exists_tac ind backtrack id continue seq =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let n=(construct_nhyps (pf_env gl) ind).(0) in
     tclIFTHENELSE
       (Tacticals.New.pf_constr_of_global id >>= simplest_elim)
@@ -207,7 +207,7 @@ let left_exists_tac ind backtrack id continue seq =
                     tclDO n intro;
                     (wrap (n-1) false continue seq)])
       backtrack
-  end }
+  end
 
 let ll_forall_tac prod backtrack id continue seq=
   tclORELSE
@@ -215,12 +215,12 @@ let ll_forall_tac prod backtrack id continue seq=
        [tclTHENLIST
 	  [intro;
            (pf_constr_of_global id >>= fun idc ->
-	   Proofview.Goal.enter { enter = begin fun gls->
+	   Proofview.Goal.enter begin fun gls->
               let open EConstr in
 	      let id0 = List.nth (pf_ids_of_hyps gls) 0 in
               let term=mkApp(idc,[|mkVar(id0)|]) in
               tclTHEN (generalize [term]) (clear [id0])
-           end });
+           end);
 	   clear_global id;
 	   intro;
 	   tclCOMPLETE (wrap 1 false continue (deepen seq))];
@@ -239,9 +239,9 @@ let defined_connectives=lazy
    AllOccurrences,EvalConstRef (fst (Term.destConst (constant "iff")))]
 
 let normalize_evaluables=
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     unfold_in_concl (Lazy.force defined_connectives) <*>
     tclMAP
       (fun id -> unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
       (pf_ids_of_hyps gl)
-  end }
+  end