Boxing the Goal.enter primitive into a record type.

4 files changed, 26 insertions, 15 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index f54d4c447..65bd32536 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -16,7 +16,7 @@ open Logic
 open Reduction
 open Tacmach
 open Clenv
-
+open Proofview.Notations
 
 (* This function put casts around metavariables whose type could not be
  * infered by the refiner, that is head of applications, predicates and
@@ -83,10 +83,10 @@ open Unification
 let dft = default_unify_flags
 
 let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let clenv gl = clenv_unique_resolver ~flags clenv gl in
     clenv_refine with_evars ~with_classes (Tacmach.New.of_old clenv (Proofview.Goal.assume gl))
-  end
+  end }
 
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
    particulier ne semblent pas vérifier que des instances différentes
@@ -118,7 +118,7 @@ let fail_quick_unif_flags = {
 
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
 let unify ?(flags=fail_quick_unif_flags) m =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let env = Tacmach.New.pf_env gl in
     let n = Tacmach.New.pf_nf_concl gl in
     let evd = clear_metas (Proofview.Goal.sigma gl) in
@@ -126,4 +126,4 @@ let unify ?(flags=fail_quick_unif_flags) m =
       let evd' = w_unify env evd CONV ~flags m n in
 	Proofview.Unsafe.tclEVARSADVANCE evd'
     with e when Errors.noncritical e -> Proofview.tclZERO e
-  end
+  end }
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 7edbef57b..b8a58daeb 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -915,6 +915,9 @@ module Goal = struct
     self : Evar.t ; (* for compatibility with old-style definitions *)
   }
 
+  type 'a enter =
+    { enter : 'a t -> unit tactic }
+
   let assume (gl : 'a t) = (gl :> [ `NF ] t)
 
   let env { env=env } = env
@@ -944,7 +947,7 @@ module Goal = struct
       tclEVARMAP >>= fun sigma ->
       try
         let (gl, sigma) = nf_gmake env sigma goal in
-        tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl))
+        tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f.enter gl))
       with e when catchable_exception e ->
         let (e, info) = Errors.push e in
         tclZERO ~info e
@@ -962,7 +965,7 @@ module Goal = struct
     gmake_with info env sigma goal
 
   let enter f =
-    let f gl = InfoL.tag (Info.DBranch) (f gl) in
+    let f gl = InfoL.tag (Info.DBranch) (f.enter gl) in
     InfoL.tag (Info.Dispatch) begin
     iter_goal begin fun goal ->
       Env.get >>= fun env ->
@@ -1054,7 +1057,7 @@ struct
   let (pr_constrv,pr_constr) =
     Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
 
-  let refine ?(unsafe = true) f = Goal.enter begin fun gl ->
+  let refine ?(unsafe = true) f = Goal.enter { Goal.enter = begin fun gl ->
     let sigma = Goal.sigma gl in
     let env = Goal.env gl in
     let concl = Goal.concl gl in
@@ -1091,7 +1094,7 @@ struct
     let open Proof in
     InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >>
     Pv.set { solution = sigma; comb; }
-  end
+  end }
 
   (** Useful definitions *)
 
@@ -1103,7 +1106,7 @@ struct
     in
     evd , j'.Environ.uj_val
 
-  let refine_casted ?unsafe f = Goal.enter begin fun gl ->
+  let refine_casted ?unsafe f = Goal.enter { Goal.enter = begin fun gl ->
     let concl = Goal.concl gl in
     let env = Goal.env gl in
     let f = { run = fun h ->
@@ -1112,7 +1115,7 @@ struct
       Sigma (c, Sigma.Unsafe.of_evar_map sigma, p)
     } in
     refine ?unsafe f
-  end
+  end }
 end
 
 
@@ -1254,6 +1257,8 @@ module Notations = struct
   let (>>=) = tclBIND
   let (<*>) = tclTHEN
   let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
+  type 'a enter = 'a Goal.enter =
+    { enter : 'a Goal.t -> unit tactic }
   type 'a s_enter = 'a Goal.s_enter =
     { s_enter : 'r. 'a Goal.t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
 end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index a94610af4..1616782e5 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -445,14 +445,17 @@ module Goal : sig
       normalised. *)
   val raw_concl : 'a t -> Term.constr
 
+  type 'a enter =
+    { enter : 'a t -> unit tactic }
+
   (** [nf_enter t] applies the goal-dependent tactic [t] in each goal
       independently, in the manner of {!tclINDEPENDENT} except that
       the current goal is also given as an argument to [t]. The goal
       is normalised with respect to evars. *)
-  val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic
+  val nf_enter : [ `NF ] enter -> unit tactic
 
   (** Like {!nf_enter}, but does not normalize the goal beforehand. *)
-  val enter : ([ `LZ ] t -> unit tactic) -> unit tactic
+  val enter : [ `LZ ] enter -> unit tactic
 
   type 'a s_enter =
     { s_enter : 'r. 'a t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
@@ -592,6 +595,8 @@ module Notations : sig
   (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *)
   val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
 
+  type 'a enter = 'a Goal.enter =
+    { enter : 'a Goal.t -> unit tactic }
   type 'a s_enter = 'a Goal.s_enter =
     { s_enter : 'r. 'a Goal.t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
 end
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 6d6215c52..fb23a28fe 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -12,6 +12,7 @@ open Pp
 open Tacexpr
 open Termops
 open Nameops
+open Proofview.Notations
 
 let (prtac, tactic_printer) = Hook.make ()
 let (prmatchpatt, match_pattern_printer) = Hook.make ()
@@ -47,10 +48,10 @@ let db_pr_goal gl =
                    str" "  ++ pc) ++ fnl ()
 
 let db_pr_goal =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let pg = db_pr_goal gl in
   Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg))
-  end
+  end }
 
 
 (* Prints the commands *)