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, 74 insertions, 87 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index d64cc38ef..05c5cd5ec 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -40,7 +40,6 @@ open Eqschemes
 open Locus
 open Locusops
 open Misctypes
-open Sigma.Notations
 open Proofview.Notations
 open Unification
 open Context.Named.Declaration
@@ -254,16 +253,16 @@ let rewrite_keyed_unif_flags = {
 }
 
 let rewrite_elim with_evars frzevars cls c e =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let flags = if Unification.is_keyed_unification ()
 	      then rewrite_keyed_unif_flags else rewrite_conv_closed_unif_flags in
   let flags = make_flags frzevars (Tacmach.New.project gl) flags c in
   general_elim_clause with_evars flags cls c e
-  end }
+  end
 
 let tclNOTSAMEGOAL tac =
   let goal gl = Proofview.Goal.goal (Proofview.Goal.assume gl) in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.nf_enter begin fun gl ->
     let sigma = project gl in
     let ev = goal gl in
     tac >>= fun () ->
@@ -278,7 +277,7 @@ let tclNOTSAMEGOAL tac =
       tclZEROMSG (str"Tactic generated a subgoal identical to the original goal.")
     else
       Proofview.tclUNIT ()
-  end }
+  end
 
 (* Ad hoc asymmetric general_elim_clause *)
 let general_elim_clause with_evars frzevars cls rew elim =
@@ -313,7 +312,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
          (general_elim_clause with_evars frzevars cls c elim))
       tac
   in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let instantiate_lemma concl =
       if not all then instantiate_lemma gl c t l l2r concl
       else instantiate_lemma_all frzevars gl c t l l2r concl
@@ -325,7 +324,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
     let cs = instantiate_lemma typ in
     if firstonly then tclFIRST (List.map try_clause cs)
     else tclMAP try_clause cs
-  end }
+  end
 
 (* The next function decides in particular whether to try a regular
   rewrite or a generalized rewrite.
@@ -387,9 +386,9 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 	     Logic.eq or Jmeq just before *)
 	assert false
     in
-      let Sigma (elim, sigma, p) = Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
+      let (sigma, elim) = fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
       let elim = EConstr.of_constr elim in
-      Sigma ((elim, Safe_typing.empty_private_constants), sigma, p)
+      (sigma, (elim, Safe_typing.empty_private_constants))
   else
   let scheme_name = match dep, lft2rgt, inccl with
     (* Non dependent case *)
@@ -407,11 +406,11 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
   | Ind (ind,u) -> 
       let c, eff = find_scheme scheme_name ind in 
       (* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *)
-      let Sigma (elim, sigma, p) =
-	Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c)
+      let (sigma, elim) =
+	fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c)
       in
       let elim = EConstr.of_constr elim in
-      Sigma ((elim, eff), sigma, p)
+      (sigma, (elim, eff))
   | _ -> assert false
 
 let type_of_clause cls gl = match cls with
@@ -419,21 +418,19 @@ let type_of_clause cls gl = match cls with
   | Some id -> pf_get_hyp_typ id gl
 
 let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
-  let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
+  Proofview.Goal.enter begin fun gl ->
+  let evd = Proofview.Goal.sigma gl in
   let isatomic = isProd evd (whd_zeta evd hdcncl) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
   let type_of_cls = type_of_clause cls gl in
   let dep = dep_proof_ok && dep_fun evd c type_of_cls in
-  let Sigma ((elim, effs), sigma, p) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
-  let tac =
+  let (sigma, (elim, effs)) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
+      Proofview.Unsafe.tclEVARS sigma <*>
       Proofview.tclEFFECTS effs <*>
       general_elim_clause with_evars frzevars tac cls c t l
       (match lft2rgt with None -> false | Some b -> b)
       {elimindex = None; elimbody = (elim,NoBindings); elimrename = None}
-  in
-  Sigma (tac, sigma, p)
-  end }
+  end
 
 let adjust_rewriting_direction args lft2rgt =
   match args with
@@ -456,7 +453,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
   if occs != AllOccurrences then (
     rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac)
   else
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       let sigma = Tacmach.New.project gl in
       let env = Proofview.Goal.env gl in
     let ctype = get_type_of env sigma c in
@@ -485,7 +482,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
 	            | None -> Proofview.tclZERO ~info e
             (* error "The provided term does not end with an equality or a declared rewrite relation." *)  
             end
-    end }
+    end
 
 let general_rewrite_ebindings =
   general_rewrite_ebindings_clause None
@@ -547,9 +544,9 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
             let ids_of_hyps = pf_ids_of_hyps gl in
 	    Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps
 	  in
-          Proofview.Goal.enter { enter = begin fun gl ->
+          Proofview.Goal.enter begin fun gl ->
             do_hyps_atleastonce (ids gl)
-          end }
+          end
 	in
 	if cl.concl_occs == NoOccurrences then do_hyps else
 	  tclIFTHENTRYELSEMUST
@@ -557,25 +554,25 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
 	   do_hyps
 
 let apply_special_clear_request clear_flag f =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
     try
-      let ((c, bl), sigma) = run_delayed env sigma f in
+      let (sigma, (c, bl)) = f env sigma in
       apply_clear_request clear_flag (use_clear_hyp_by_default ()) c
     with
       e when catchable_exception e -> tclIDTAC
-  end }
+  end
 
 let general_multi_rewrite with_evars l cl tac =
   let do1 l2r f =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       let sigma = Tacmach.New.project gl in
       let env = Proofview.Goal.env gl in
-      let (c, sigma) = run_delayed env sigma f in
+      let (sigma, c) = f env sigma in
       tclWITHHOLES with_evars
         (general_rewrite_clause l2r with_evars ?tac c cl) sigma
-    end }
+    end
   in
   let rec doN l2r c = function
     | Precisely n when n <= 0 -> Proofview.tclUNIT ()
@@ -638,7 +635,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
       | None -> Proofview.tclUNIT ()
       | Some tac ->  tclCOMPLETE tac
   in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let get_type_of = pf_apply get_type_of gl in
   let t1 = get_type_of c1
   and t2 = get_type_of c2 in
@@ -664,7 +661,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
           tclTHEN (apply sym) assumption;
           try_prove_eq
          ])
-  end }
+  end
 
 let replace c1 c2 =
   replace_using_leibniz onConcl c2 c1 false false None
@@ -934,13 +931,9 @@ let build_selector env sigma dirn c ind special default =
   let ci = make_case_info env ind RegularStyle in
   sigma, mkCase (ci, p, c, Array.of_list brl)
 
-let new_global sigma gr =
-  let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr
-  in Sigma.to_evar_map sigma, c
-    
-let build_coq_False sigma = new_global sigma (build_coq_False ())
-let build_coq_True sigma = new_global sigma (build_coq_True ())
-let build_coq_I sigma = new_global sigma (build_coq_I ())
+let build_coq_False sigma = Evarutil.new_global sigma (build_coq_False ())
+let build_coq_True sigma = Evarutil.new_global sigma (build_coq_True ())
+let build_coq_I sigma = Evarutil.new_global sigma (build_coq_I ())
 
 let rec build_discriminator env sigma dirn c = function
   | [] ->
@@ -967,7 +960,7 @@ let rec build_discriminator env sigma dirn c = function
 *)
 
 let gen_absurdity id =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let sigma = project gl in
   let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in
   if is_empty_type sigma hyp_typ
@@ -975,7 +968,7 @@ let gen_absurdity id =
     simplest_elim (mkVar id)
   else
     tclZEROMSG (str "Not the negation of an equality.")
-  end }
+  end
 
 (* Precondition: eq is leibniz equality
 
@@ -1032,17 +1025,17 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
 
 let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     match find_positions env sigma ~no_discr:false t1 t2 with
     | Inr _ ->
 	tclZEROMSG (str"Not a discriminable equality.")
     | Inl (cpath, (_,dirn), _) ->
 	discr_positions env sigma u eq_clause cpath dirn
-  end }
+  end
 
 let onEquality with_evars tac (c,lbindc) =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let type_of = pf_unsafe_type_of gl in
   let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
   let t = type_of c in
@@ -1054,10 +1047,10 @@ let onEquality with_evars tac (c,lbindc) =
   tclTHEN
     (Proofview.Unsafe.tclEVARS eq_clause'.evd)
     (tac (eq,eqn,eq_args) eq_clause')
-  end }
+  end
 
 let onNegatedEquality with_evars tac =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let ccl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
@@ -1068,7 +1061,7 @@ let onNegatedEquality with_evars tac =
             onEquality with_evars tac (mkVar id,NoBindings)))
     | _ ->
         tclZEROMSG (str "Not a negated primitive equality.")
-  end }
+  end
 
 let discrSimpleClause with_evars = function
   | None -> onNegatedEquality with_evars discrEq
@@ -1327,7 +1320,7 @@ let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined")
 let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
 
 let inject_if_homogenous_dependent_pair ty =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   try
     let sigma = Tacmach.New.project gl in
     let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
@@ -1367,7 +1360,7 @@ let inject_if_homogenous_dependent_pair ty =
           ])]
   with Exit ->
     Proofview.tclUNIT ()
-  end }
+  end
 
 (* Given t1=t2 Inj calculates the whd normal forms of t1 and t2 and it
    expands then only when the whdnf has a constructor of an inductive type
@@ -1451,7 +1444,7 @@ let injEq ?(old=false) with_evars clear_flag ipats =
   let post_tac c n =
     match ipats_style with
     | Some ipats ->
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let sigma = project gl in
         let destopt = match EConstr.kind sigma c with
         | Var id -> get_previous_hyp_position id gl
@@ -1464,7 +1457,7 @@ let injEq ?(old=false) with_evars clear_flag ipats =
           then intro_patterns_bound_to with_evars n destopt ipats
           else intro_patterns_to with_evars destopt ipats in
         tclTHEN clear_tac intro_tac
-      end }
+      end
     | None -> tclIDTAC in
   injEqThen post_tac l2r
 
@@ -1482,7 +1475,7 @@ let injConcl = injClause None false None
 let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.tag id)))
 
 let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma =  clause.evd in
     let env = Proofview.Goal.env gl in
       match find_positions env sigma ~no_discr:false t1 t2 with
@@ -1493,7 +1486,7 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
     | Inr posns ->
 	inject_at_positions env sigma true u clause posns
           (ntac (clenv_value clause))
-  end }
+  end
 
 let dEqThen with_evars ntac = function
   | None -> onNegatedEquality with_evars (decompEqThen (ntac None))
@@ -1504,10 +1497,10 @@ let dEq with_evars =
     (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
 
 let intro_decomp_eq tac data (c, t) =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in
     decompEqThen (fun _ -> tac) data cl
-  end }
+  end
 
 let _ = declare_intro_decomp_eq intro_decomp_eq
 
@@ -1558,7 +1551,6 @@ let decomp_tuple_term env sigma c t =
   in decomprec (mkRel 1) c t
 
 let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
-  let sigma = Sigma.to_evar_map sigma in
   let typ = get_type_of env sigma dep_pair1 in
   (* We find all possible decompositions *)
   let decomps1 = decomp_tuple_term env sigma dep_pair1 typ in
@@ -1583,7 +1575,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   (* Retype to get universes right *)
   let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in
   let sigma, _ = Typing.type_of env sigma body in
-  Sigma.Unsafe.of_pair ((body, expected_goal), sigma)
+  (sigma, (body, expected_goal))
 
 (* Like "replace" but decompose dependent equalities                      *)
 (* i.e. if equality is "exists t v = exists u w", and goal is "phi(t,u)", *)
@@ -1591,42 +1583,38 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
 (* on for further iterated sigma-tuples                                   *)
 
 let cutSubstInConcl l2r eqn =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
   let typ = pf_concl gl in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
-  let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
-  let tac =
-  tclTHENFIRST
+  let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in
+  tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+  (tclTHENFIRST
     (tclTHENLIST [
        (change_concl typ); (* Put in pattern form *)
        (replace_core onConcl l2r eqn)
     ])
-    (change_concl expected) (* Put in normalized form *)
-  in
-  Sigma (tac, sigma, p)
-  end }
+    (change_concl expected)) (* Put in normalized form *)
+  end
 
 let cutSubstInHyp l2r eqn id =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
   let typ = pf_get_hyp_typ id gl in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
-  let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
-  let tac =
-    tclTHENFIRST
+  let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in
+  tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+    (tclTHENFIRST
     (tclTHENLIST [
        (change_in_hyp None (make_change_arg typ) (id,InHypTypeOnly));
        (replace_core (onHyp id) l2r eqn)
     ])
-    (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly))
-  in
-  Sigma (tac, sigma, p)
-  end }
+    (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly)))
+  end
 
 let try_rewrite tac =
   Proofview.tclORELSE tac begin function (e, info) -> match e with
@@ -1648,11 +1636,11 @@ let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id)
 let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
 
 let substClause l2r c cls =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let eq = pf_apply get_type_of gl c in
   tclTHENS (cutSubstClause l2r eq cls)
     [Proofview.tclUNIT (); exact_no_check c]
-  end }
+  end
 
 let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls)
 let rewriteInHyp l2r c id = rewriteClause l2r c (Some id)
@@ -1713,7 +1701,7 @@ let is_eq_x gl x d =
    erase hyp and x; proceed by generalizing all dep hyps *)
 
 let subst_one dep_proof_ok x (hyp,rhs,dir) =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
@@ -1742,13 +1730,13 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
       else
        [Proofview.tclUNIT ()]) @
      [tclTRY (clear [x; hyp])])
-  end }
+  end
 
 (* Look for an hypothesis hyp of the form "x=rhs" or "rhs=x", rewrite
    it everywhere, and erase hyp and x; proceed by generalizing all dep hyps *)
 
 let subst_one_var dep_proof_ok x =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let gl = Proofview.Goal.assume gl in
     let decl = pf_get_hyp x gl in
     (* If x has a body, simply replace x with body and clear x *)
@@ -1765,7 +1753,7 @@ let subst_one_var dep_proof_ok x =
 	       str".")
         with FoundHyp res -> res in
       subst_one dep_proof_ok x res
-  end }
+  end
 
 let subst_gen dep_proof_ok ids =
   tclMAP (subst_one_var dep_proof_ok) ids
@@ -1818,7 +1806,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
 
   (* Second step: treat equations *)
   let process hyp =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let gl = Proofview.Goal.assume gl in
     let sigma = project gl in
     let env = Proofview.Goal.env gl in
@@ -1834,19 +1822,19 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
           subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
       | _ ->
           Proofview.tclUNIT ()
-    end }
+    end
   in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let ids = find_equations gl in
     tclMAP process ids
-  end }
+  end
 
   else
 
 (* Old implementation, not able to manage configurations like a=b, a=t,
    or situations like "a = S b, b = S a", or also accidentally unfolding
    let-ins *)
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let sigma = project gl in
   let find_eq_data_decompose = find_eq_data_decompose gl in
   let test (_,c) =
@@ -1865,7 +1853,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
   let ids = List.map_filter test hyps in
   let ids = List.uniquize ids in
   subst_gen flags.rewrite_dependent_proof ids
-  end }
+  end
 
 (* Rewrite the first assumption for which a condition holds
    and gives the direction of the rewrite *)
@@ -1902,11 +1890,10 @@ let rewrite_assumption_cond cond_eq_term cl =
 	  with | Failure _ | UserError _ -> arec rest gl
 	end
   in
-  Proofview.Goal.enter { enter = begin fun gl ->
-    let gl = Proofview.Goal.lift gl Sigma.Unsafe.le in
+  Proofview.Goal.enter begin fun gl ->
     let hyps = Proofview.Goal.hyps gl in
     arec hyps gl
-  end }
+  end
 
 (* Generalize "subst x" to substitution of subterm appearing as an
    equation in the context, but not clearing the hypothesis *)