diff options
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 7edbef57b4..b8a58daeb2 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 |