diff options
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index cf4224bbdb..a725444e81 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -39,7 +39,7 @@ let proofview p = let compact el ({ solution } as pv) = let nf c = Evarutil.nf_evar solution c in - let nf0 c = EConstr.(to_constr solution (of_constr c)) in + let nf0 c = EConstr.(to_constr ~abort_on_undefined_evars:false solution (of_constr c)) in let size = Evd.fold (fun _ _ i -> i+1) solution 0 in let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in let pruned_solution = Evd.drop_all_defined solution in @@ -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 |