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, 20 insertions, 20 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index b99ccbf4a..9e6e5e313 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -365,7 +365,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
         )))
       )
   in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in
     let sigma = Tacmach.New.project gl in
     let u,v = destruct_ind sigma type_of_pq
@@ -397,7 +397,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
            Tacticals.New.tclTHENLIST [
              Proofview.tclEFFECTS eff;
              Equality.replace p q ; apply app ; Auto.default_auto]
-  end }
+  end
 
 (* used in the bool -> leib side *)
 let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
@@ -430,7 +430,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
   let rec aux l1 l2 =
     match (l1,l2) with
     | (t1::q1,t2::q2) ->
-        Proofview.Goal.enter { enter = begin fun gl ->
+        Proofview.Goal.enter begin fun gl ->
         let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
         let sigma = Tacmach.New.project gl in
         if EConstr.eq_constr sigma t1 t2 then aux q1 q2
@@ -472,7 +472,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
                   aux q1 q2 ]
               )
         )
-        end }
+        end
     | ([],[]) -> Proofview.tclUNIT ()
     | _ -> Tacticals.New.tclZEROMSG (str "Both side of the equality must have the same arity.")
   in
@@ -581,7 +581,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
           let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
           avoid := fresh::(!avoid); fresh
       in
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
       let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
       let freshn = fresh_id (Id.of_string "x") gl in
       let freshm = fresh_id (Id.of_string "y") gl in
@@ -604,18 +604,18 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                     Tacticals.New.tclREPEAT (
                       Tacticals.New.tclTHENLIST [
                          Simple.apply_in freshz (EConstr.of_constr (andb_prop()));
-                         Proofview.Goal.enter { enter = begin fun gl ->
+                         Proofview.Goal.enter begin fun gl ->
                            let fresht = fresh_id (Id.of_string "Z") gl in
                             destruct_on_as (EConstr.mkVar freshz)
                                   (IntroOrPattern [[Loc.tag @@ IntroNaming (IntroIdentifier fresht);
                                     Loc.tag @@ IntroNaming (IntroIdentifier freshz)]])
-                         end }
+                         end
                         ]);
 (*
   Ci a1 ... an = Ci b1 ... bn
  replace bi with ai; auto || replace bi with ai by  apply typeofbi_prod ; auto
 *)
-                      Proofview.Goal.enter { enter = begin fun gl ->
+                      Proofview.Goal.enter begin fun gl ->
                         let concl = Proofview.Goal.concl gl in
                         let sigma = Tacmach.New.project gl in
                         match EConstr.kind sigma concl with
@@ -635,10 +635,10 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                           | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.")
                         )
                         | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.")
-                      end }
+                      end
 
                     ]
-      end }
+      end
 
 let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
 
@@ -725,7 +725,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
           let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
           avoid := fresh::(!avoid); fresh
       in
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
       let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
       let freshn = fresh_id (Id.of_string "x") gl in
       let freshm = fresh_id (Id.of_string "y") gl in
@@ -748,7 +748,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
                       Tacticals.New.tclTHENLIST [apply (EConstr.of_constr (andb_true_intro()));
                                   simplest_split ;Auto.default_auto ]
                       );
-                      Proofview.Goal.enter { enter = begin fun gls ->
+                      Proofview.Goal.enter begin fun gls ->
                         let concl = Proofview.Goal.concl gls in
                         let sigma = Tacmach.New.project gl in
                         (* assume the goal to be eq (eq_type ...) = true *)
@@ -765,9 +765,9 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
                         )
                         | _ ->
                             Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.")
-                      end }
+                      end
                     ]
-      end }
+      end
 
 let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
 
@@ -873,7 +873,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
       let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
       avoid := fresh::(!avoid); fresh
   in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
   let freshn = fresh_id (Id.of_string "x") gl in
   let freshm = fresh_id (Id.of_string "y") gl in
@@ -904,7 +904,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
 	))
 	  (Tacticals.New.tclTHEN (destruct_on (EConstr.of_constr eqbnm)) Auto.default_auto);
 
-        Proofview.Goal.enter { enter = begin fun gl ->
+        Proofview.Goal.enter begin fun gl ->
           let freshH2 = fresh_id (Id.of_string "H") gl in
 	  Tacticals.New.tclTHENS (destruct_on_using (EConstr.mkVar freshH) freshH2) [
 	    (* left *)
@@ -916,7 +916,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
             ;
 
 	    (*right *)
-            Proofview.Goal.enter { enter = begin fun gl ->
+            Proofview.Goal.enter begin fun gl ->
             let freshH3 = fresh_id (Id.of_string "H") gl in
             Tacticals.New.tclTHENLIST [
 	      simplest_right ;
@@ -938,11 +938,11 @@ let compute_dec_tact ind lnamesparrec nparrec =
                               true;
               Equality.discr_tac false None
 	    ]
-            end }
+            end
 	  ]
-        end }
+        end
   ]
-  end }
+  end
 
 let make_eq_decidability mode mind =
   let mib = Global.lookup_mind mind in