Boxing the Goal.enter primitive into a record type.

1 files changed, 19 insertions, 19 deletions

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 }