Boxing the Goal.enter primitive into a record type.

1 files changed, 20 insertions, 20 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 8ac273c84f..8282ce30be 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -355,7 +355,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
         )))
       )
   in
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
     let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in
     let u,v = destruct_ind type_of_pq
     in let lb_type_of_p =
@@ -385,7 +385,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 =
@@ -417,7 +417,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 begin fun gl ->
+        Proofview.Goal.enter { enter = begin fun gl ->
         let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
         if eq_constr t1 t2 then aux q1 q2
         else (
@@ -458,7 +458,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
@@ -565,7 +565,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
           avoid := fresh::(!avoid); fresh
         end gl
       in
-      Proofview.Goal.nf_enter begin fun gl ->
+      Proofview.Goal.nf_enter { 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
@@ -588,18 +588,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 (andb_prop());
-                         Proofview.Goal.nf_enter begin fun gl ->
+                         Proofview.Goal.nf_enter { enter = begin fun gl ->
                            let fresht = fresh_id (Id.of_string "Z") gl in
                             (destruct_on_as (mkVar freshz)
                                   [[dl,IntroNaming (IntroIdentifier fresht);
                                     dl,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.nf_enter begin fun gls ->
+                      Proofview.Goal.nf_enter { enter = begin fun gls ->
                         let gl = Proofview.Goal.concl gls in
                         match (kind_of_term gl) with
                         | App (c,ca) -> (
@@ -618,10 +618,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")
 
@@ -708,7 +708,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
           avoid := fresh::(!avoid); fresh
         end gl
       in
-      Proofview.Goal.nf_enter begin fun gl ->
+      Proofview.Goal.nf_enter { 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
@@ -731,7 +731,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
                       Tacticals.New.tclTHENLIST [apply (andb_true_intro());
                                   simplest_split ;Auto.default_auto ]
                       );
-                      Proofview.Goal.nf_enter begin fun gls ->
+                      Proofview.Goal.nf_enter { enter = begin fun gls ->
                         let gl = Proofview.Goal.concl gls in
                         (* assume the goal to be eq (eq_type ...) = true *)
                         match (kind_of_term gl) with
@@ -747,9 +747,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")
 
@@ -855,7 +855,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
       avoid := fresh::(!avoid); fresh
     end gl
   in
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { 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
@@ -886,7 +886,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
 	)
 	  (Tacticals.New.tclTHEN (destruct_on eqbnm) Auto.default_auto);
 
-        Proofview.Goal.nf_enter begin fun gl ->
+        Proofview.Goal.nf_enter { enter = begin fun gl ->
           let freshH2 = fresh_id (Id.of_string "H") gl in
 	  Tacticals.New.tclTHENS (destruct_on_using (mkVar freshH) freshH2) [
 	    (* left *)
@@ -898,7 +898,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
             ;
 
 	    (*right *)
-            Proofview.Goal.nf_enter begin fun gl ->
+            Proofview.Goal.nf_enter { enter = begin fun gl ->
             let freshH3 = fresh_id (Id.of_string "H") gl in
             Tacticals.New.tclTHENLIST [
 	      simplest_right ;
@@ -920,11 +920,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