diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/proofview.ml | 12 | ||||
| -rw-r--r-- | engine/proofview.mli | 17 | ||||
| -rw-r--r-- | engine/proofview_monad.ml | 9 | ||||
| -rw-r--r-- | engine/proofview_monad.mli | 2 |
4 files changed, 28 insertions, 12 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index d4ad53ff5f..a725444e81 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -223,9 +223,9 @@ module Proof = Logical type +'a tactic = 'a Proof.t (** Applies a tactic to the current proofview. *) -let apply env t sp = +let apply ~name ~poly env t sp = let open Logic_monad in - let ans = Proof.repr (Proof.run t false (sp,env)) in + let ans = Proof.repr (Proof.run t P.{trace=false; name; poly} (sp,env)) in let ans = Logic_monad.NonLogical.run ans in match ans with | Nil (e, info) -> iraise (TacticFailure e, info) @@ -993,7 +993,10 @@ let tclTIME s t = tclOR (tclUNIT x) (fun e -> aux (n+1) (k e)) in aux 0 t - +let tclProofInfo = + let open Proof in + Logical.current >>= fun P.{name; poly} -> + tclUNIT (name, poly) (** {7 Unsafe primitives} *) @@ -1275,7 +1278,8 @@ module V82 = struct let of_tactic t gls = try let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in - let (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in + let name, poly = Names.Id.of_string "legacy_pe", false in + let (_,final,_,_) = apply ~name ~poly (goal_env gls.Evd.sigma gls.Evd.it) t init in { Evd.sigma = final.solution ; it = CList.map drop_state final.comb } with Logic_monad.TacticFailure e as src -> let (_, info) = CErrors.push src in diff --git a/engine/proofview.mli b/engine/proofview.mli index 286703c0dc..680a93f0cc 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -156,10 +156,15 @@ type +'a tactic tactic has given up. In case of multiple success the first one is selected. If there is no success, fails with {!Logic_monad.TacticFailure}*) -val apply : Environ.env -> 'a tactic -> proofview -> 'a - * proofview - * (bool*Evar.t list*Evar.t list) - * Proofview_monad.Info.tree +val apply + : name:Names.Id.t + -> poly:bool + -> Environ.env + -> 'a tactic + -> proofview + -> 'a * proofview + * (bool*Evar.t list*Evar.t list) + * Proofview_monad.Info.tree (** {7 Monadic primitives} *) @@ -407,6 +412,10 @@ val tclTIMEOUT : int -> 'a tactic -> 'a tactic identifying annotation if present *) val tclTIME : string option -> 'a tactic -> 'a tactic +(** Internal, don't use. *) +val tclProofInfo : (Names.Id.t * bool) tactic +[@@ocaml.deprecated "internal, don't use"] + (** {7 Unsafe primitives} *) (** The primitives in the [Unsafe] module should be avoided as much as diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml index 69341d97df..80eb9d0124 100644 --- a/engine/proofview_monad.ml +++ b/engine/proofview_monad.ml @@ -177,7 +177,7 @@ module P = struct type s = proofview * Environ.env (** Recording info trace (true) or not. *) - type e = bool + type e = { trace: bool; name : Names.Id.t; poly : bool } (** Status (safe/unsafe) * shelved goals * given up *) type w = bool * goal list @@ -254,13 +254,16 @@ end (** Lens and utilies pertaining to the info trace *) module InfoL = struct - let recording = Logical.current + let recording = Logical.(map (fun {P.trace} -> trace) current) let if_recording t = let open Logical in recording >>= fun r -> if r then t else return () - let record_trace t = Logical.local true t + let record_trace t = + Logical.( + current >>= fun s -> + local {s with P.trace = true} t) let raw_update = Logical.update let update f = if_recording (raw_update f) diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index a08cab3bf6..3437b6ce77 100644 --- a/engine/proofview_monad.mli +++ b/engine/proofview_monad.mli @@ -98,7 +98,7 @@ module P : sig val wprod : w -> w -> w (** Recording info trace (true) or not. *) - type e = bool + type e = { trace: bool; name : Names.Id.t; poly : bool } type u = Info.state |