Boxing the Goal.enter primitive into a record type.

7 files changed, 61 insertions, 62 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 57268a9cf..5a49fc8f4 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -1,3 +1,4 @@
+open Proofview.Notations
 
 let contrib_name = "btauto"
 
@@ -216,7 +217,7 @@ module Btauto = struct
     Tacticals.tclFAIL 0 msg gl
 
   let try_unification env =
-    Proofview.Goal.nf_enter begin fun gl ->
+    Proofview.Goal.nf_enter { enter = begin fun gl ->
       let concl = Proofview.Goal.concl gl in
       let eq = Lazy.force eq in
       let t = decomp_term concl in
@@ -228,10 +229,10 @@ module Btauto = struct
       | _ ->
           let msg = str "Btauto: Internal error" in
           Tacticals.New.tclFAIL 0 msg
-    end
+    end }
 
   let tac =
-    Proofview.Goal.nf_enter begin fun gl ->
+    Proofview.Goal.nf_enter { enter = begin fun gl ->
       let concl = Proofview.Goal.concl gl in
       let eq = Lazy.force eq in
       let bool = Lazy.force Bool.typ in
@@ -255,6 +256,6 @@ module Btauto = struct
       | _ ->
           let msg = str "Cannot recognize a boolean equality" in
           Tacticals.New.tclFAIL 0 msg
-    end
+    end }
 
 end
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 068cb25cf..35178aa1e 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -22,6 +22,7 @@ open Ccproof
 open Pp
 open Errors
 open Util
+open Proofview.Notations
 
 let reference dir s = lazy (Coqlib.gen_reference "CC" dir s)
 
@@ -254,13 +255,13 @@ let new_app_global f args k =
 let new_refine c = Proofview.V82.tactic (refine c)
 
 let assert_before n c =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let evm, _ = Tacmach.New.pf_apply type_of gl c in
       Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c)
-  end
+  end }
     
 let rec proof_tac p : unit Proofview.tactic =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
   try (* type_of can raise exceptions *)
   match p.p_rule with
@@ -325,10 +326,10 @@ let rec proof_tac p : unit Proofview.tactic =
            app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in
 	   Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf)
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-  end
+  end }
 
 let refute_tac c t1 t2 p =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let intype =
     Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt1)) gl
@@ -338,14 +339,14 @@ let refute_tac c t1 t2 p =
   let false_t=mkApp (c,[|mkVar hid|]) in
     Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
       [proof_tac p; simplest_elim false_t]
-  end
+  end }
 
 let refine_exact_check c gl =
   let evm, _ = pf_apply type_of gl c in
     Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
 
 let convert_to_goal_tac c t1 t2 p = 
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let sort =
     Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt2)) gl
@@ -357,20 +358,20 @@ let convert_to_goal_tac c t1 t2 p =
   let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
       [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
-  end
+  end }
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let tt2=constr_of_term t2 in
   let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in
   let false_t=mkApp (c2,[|mkVar h|]) in
     Tacticals.New.tclTHENS (assert_before (Name h) tt2)
       [convert_to_goal_tac c1 t1 t2 p;
        simplest_elim false_t]
-  end
+  end }
 
 let discriminate_tac (cstr,u as cstru) p =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
     let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
     let intype =
       Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls t1)) gl
@@ -399,7 +400,7 @@ let discriminate_tac (cstr,u as cstru) p =
     Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)
       (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
         [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)])
-  end
+  end }
 
 (* wrap everything *)
 
@@ -411,7 +412,7 @@ let build_term_to_complete uf meta pac =
     applistc (mkConstructU cinfo.ci_constr) all_args
 
 let cc_tactic depth additionnal_terms =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
     Coqlib.check_required_library Coqlib.logic_module_name;
     let _ = debug (Pp.str "Reading subgoal ...") in
     let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in
@@ -462,7 +463,7 @@ let cc_tactic depth additionnal_terms =
 		convert_to_goal_tac id ta tb p
 	    | HeqnH (ida,idb) ->
 		convert_to_hyp_tac ida ta idb tb p
-  end
+  end }
 
 let cc_fail gls =
   errorlabstrm  "Congruence" (Pp.str "congruence failed.")
@@ -485,8 +486,7 @@ let congruence_tac depth l =
     
 let mk_eq f c1 c2 k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
-  Proofview.Goal.enter begin
-    fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let open Tacmach.New in
     let evm, ty = pf_apply type_of gl c1 in
     let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in
@@ -494,10 +494,10 @@ let mk_eq f c1 c2 k =
     let evm, _ =  type_of (pf_env gl) evm term in
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
 			  (k term)
-    end)
+    end })
     
 let f_equal =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let cut_eq c1 c2 =
       try (* type_of can raise an exception *)
@@ -523,4 +523,4 @@ let f_equal =
         | Type_errors.TypeError _ -> Proofview.tclUNIT ()
         | e -> Proofview.tclZERO ~info e
       end
-  end
+  end }
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 7a56cd665..e5c9b2707 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -19,6 +19,7 @@ open Globnames
 open Tacmach
 open Fourier
 open Contradiction
+open Proofview.Notations
 
 (******************************************************************************
 Opérations sur les combinaisons linéaires affines.
@@ -462,7 +463,7 @@ exception GoalDone
 
 (* Résolution d'inéquations linéaires dans R *)
 let rec fourier () =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
     let goal = strip_outer_cast concl in
@@ -622,7 +623,7 @@ let rec fourier () =
 (*    ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *)
       !tac
 (*      ((tclABSTRACT None !tac) gl) *)
-  end
+  end }
 ;;
 
 (*
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index ef1169342..a0e61623c 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -20,6 +20,7 @@ open Pp
 open Mutils
 open Proofview
 open Goptions
+open Proofview.Notations
 
 (**
   * Debug flag 
@@ -1444,8 +1445,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
  let ff  = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
  let vm = dump_varmap (spec.typ) env in
  (* todo : directly generate the proof term - or generalize before conversion? *)
-  Proofview.Goal.nf_enter
-  begin fun gl -> 
+  Proofview.Goal.nf_enter { enter = begin fun gl -> 
    Tacticals.New.tclTHENLIST
     [
      Tactics.change_concl
@@ -1462,7 +1462,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
    Tactics.new_generalize env ;
    Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
   ] 
-  end
+  end }
 
 
 (**
@@ -1707,9 +1707,7 @@ let micromega_gen
     (normalise:'cst atom -> 'cst mc_cnf)
     unsat deduce 
     spec prover =
- Proofview.Goal.nf_enter
-  begin 
-   fun gl -> 
+ Proofview.Goal.nf_enter { enter = begin fun gl -> 
     let concl = Tacmach.New.pf_concl gl in
     let hyps  = Tacmach.New.pf_hyps_types gl in
     try
@@ -1735,7 +1733,7 @@ let micromega_gen
                             ^ "the use of a specialized external tool called csdp. \n\n" 
                             ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n"
                             ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp"))
-  end
+  end }
 
 let micromega_gen parse_arith 
     (negate:'cst atom -> 'cst mc_cnf)
@@ -1756,9 +1754,7 @@ let micromega_order_changer cert env ff  =
  let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in
  let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
  let vm = dump_varmap (typ) env in
- Proofview.Goal.nf_enter
-  begin 
-   fun gl -> 
+ Proofview.Goal.nf_enter { enter = begin fun gl -> 
     Tacticals.New.tclTHENLIST
      [
      (Tactics.change_concl
@@ -1774,7 +1770,7 @@ let micromega_order_changer cert env ff  =
       Tactics.new_generalize env ;
       Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
      ]
-  end
+  end }
 
 
 let micromega_genr prover =
@@ -1790,9 +1786,7 @@ let micromega_genr prover =
     proof_typ = Lazy.force coq_QWitness ;
     dump_proof = dump_psatz coq_Q dump_q
   } in
-  Proofview.Goal.nf_enter
-   begin 
-    fun gl -> 
+  Proofview.Goal.nf_enter { enter = begin fun gl -> 
      let concl = Tacmach.New.pf_concl gl in
      let hyps  = Tacmach.New.pf_hyps_types gl in
      try
@@ -1822,7 +1816,7 @@ let micromega_genr prover =
       ^ "the use of a specialized external tool called csdp. \n\n" 
       ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n"
        ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp"))
-    end
+    end }
 
 
 let micromega_genr prover  = (micromega_genr prover)
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index aac9a7d31..976ab949c 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -27,6 +27,7 @@ open Globnames
 open Nametab
 open Contradiction
 open Misctypes
+open Proofview.Notations
 
 module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
@@ -34,9 +35,9 @@ open OmegaSolver
 (* Added by JCF, 09/03/98 *)
 
 let elim_id id =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
     simplest_elim (Tacmach.New.pf_global id gl)
-  end
+  end }
 let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl
 
 let timing timer_name f arg = f arg
@@ -1416,7 +1417,7 @@ let reintroduce id =
 open Proofview.Notations
 
 let coq_omega =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   clear_constr_tables ();
   let hyps_types = Tacmach.New.pf_hyps_types gl in
   let destructure_omega = Tacmach.New.of_old destructure_omega gl in
@@ -1464,12 +1465,12 @@ let coq_omega =
       Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path)
     with NO_CONTRADICTION -> Tacticals.New.tclZEROMSG (Pp.str"Omega can't solve this system")
   end
-  end
+  end }
 
 let coq_omega = coq_omega
 
 let nat_inject =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in
   let rec explore p t : unit Proofview.tactic =
     try match destructurate_term t with
@@ -1603,7 +1604,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
@@ -1673,22 +1674,22 @@ let onClearedName id tac =
   (* so renaming may be necessary *)
   Tacticals.New.tclTHEN
     (Proofview.V82.tactic (tclTRY (clear [id])))
-    (Proofview.Goal.nf_enter begin fun gl ->
+    (Proofview.Goal.nf_enter { enter = begin fun gl ->
      let id = Tacmach.New.of_old (fresh_id [] id) gl in
      Tacticals.New.tclTHEN (introduction id) (tac id)
-    end)
+    end })
 
 let onClearedName2 id tac =
   Tacticals.New.tclTHEN
     (Proofview.V82.tactic (tclTRY (clear [id])))
-    (Proofview.Goal.nf_enter begin fun gl ->
+    (Proofview.Goal.nf_enter { enter = begin fun gl ->
      let id1 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) gl in
      let id2 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) gl in
       Tacticals.New.tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
-    end)
+    end })
 
 let destructure_hyps =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let type_of = Tacmach.New.pf_unsafe_type_of gl in
   let decidability = Tacmach.New.of_old decidability gl in
   let pf_nf = Tacmach.New.of_old pf_nf gl in
@@ -1828,10 +1829,10 @@ let destructure_hyps =
     in
     let hyps = Proofview.Goal.hyps gl in
     loop hyps
-  end
+  end }
 
 let destructure_goal =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let decidability = Tacmach.New.of_old decidability gl in
     let rec loop t =
@@ -1855,7 +1856,7 @@ let destructure_goal =
 	  Tacticals.New.tclTHEN goal_tac destructure_hyps
     in
     (loop concl)
-  end
+  end }
 
 let destructure_goal = destructure_goal
 
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 2a2ef30fb..8d60b8ba2 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -109,6 +109,7 @@ open Pattern
 open Patternops
 open Constr_matching
 open Tacmach
+open Proofview.Notations
 (*i*)
 
 (*s First, we need to access some Coq constants
@@ -446,7 +447,7 @@ let quote_terms ivs lc =
   yet. *)
 
 let quote f lid =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
     let f = Tacmach.New.pf_global f gl in
     let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
     let ivs = compute_ivs f cl gl in
@@ -459,10 +460,10 @@ let quote f lid =
     match ivs.variable_lhs with
     | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast
     | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast
-  end
+  end }
 
 let gen_quote cont c f lid =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let f = Tacmach.New.pf_global f gl in
   let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
   let ivs = compute_ivs f cl gl in
@@ -474,7 +475,7 @@ let gen_quote cont c f lid =
   match ivs.variable_lhs with
     | None -> cont (mkApp (f, [| p |]))
     | Some _ -> cont (mkApp (f, [| vm; p |]))
-  end
+  end }
 
 (*i
 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 942ca15a5..8ff4230e8 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -31,6 +31,7 @@ open Decl_kinds
 open Entries
 open Misctypes
 open Newring_ast
+open Proofview.Notations
 
 (****************************************************************************)
 (* controlled reduction *)
@@ -747,7 +748,7 @@ let ltac_ring_structure e =
    lemma1;lemma2;pretac;posttac]
 
 let ring_lookup (f:glob_tactic_expr) lH rl t =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     try (* find_ring_strucure can raise an exception *)
@@ -759,7 +760,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t =
       let ring = ltac_ring_structure e in
       Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl]))
     with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-  end
+  end }
 
 (***********************************************************************)
 
@@ -1019,7 +1020,7 @@ let ltac_field_structure e =
    field_simpl_eq_in_ok;cond_ok;pretac;posttac]
 
 let field_lookup (f:glob_tactic_expr) lH rl t =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     try
@@ -1031,4 +1032,4 @@ let field_lookup (f:glob_tactic_expr) lH rl t =
       let field = ltac_field_structure e in
       Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl]))
     with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-  end
+  end }