aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.mlg7
-rw-r--r--plugins/ltac/g_auto.mlg3
-rw-r--r--plugins/ltac/rewrite.ml4
-rw-r--r--plugins/ltac/tacinterp.ml80
4 files changed, 72 insertions, 22 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 47f593ff3e..ffd8b71e5d 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -50,7 +50,8 @@ let with_delayed_uconstr ist c tac =
Pretyping.use_typeclasses = false;
solve_unification_constraints = true;
fail_evar = false;
- expand_evars = true
+ expand_evars = true;
+ program_mode = false;
} in
let c = Tacinterp.type_uconstr ~flags ist c in
Tacticals.New.tclDELAYEDWITHHOLES false c tac
@@ -344,7 +345,9 @@ let constr_flags () = {
Pretyping.use_typeclasses = true;
Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
Pretyping.fail_evar = false;
- Pretyping.expand_evars = true }
+ Pretyping.expand_evars = true;
+ Pretyping.program_mode = false;
+}
let refine_tac ist simple with_classes c =
Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 7be8f67616..663537f3e8 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -56,7 +56,8 @@ let eval_uconstrs ist cs =
Pretyping.use_typeclasses = false;
solve_unification_constraints = true;
fail_evar = false;
- expand_evars = true
+ expand_evars = true;
+ program_mode = false;
} in
let map c env sigma = c env sigma in
List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2055b25ff4..7da4464e59 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1889,7 +1889,7 @@ let declare_projection n instance_id r =
in it_mkProd_or_LetIn ccl ctx
in
let typ = it_mkProd_or_LetIn typ ctx in
- let univs = Evd.const_univ_entry ~poly sigma in
+ let univs = Evd.univ_entry ~poly sigma in
let typ = EConstr.to_constr sigma typ in
let term = EConstr.to_constr sigma term in
let cst =
@@ -1975,7 +1975,7 @@ let add_morphism_infer atts m n =
let evd = Evd.from_env env in
let uctx, instance = build_morphism_signature env evd m in
if Lib.is_modtype () then
- let uctx = UState.const_univ_entry ~poly:atts.polymorphic uctx in
+ let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
(Entries.ParameterEntry
(None,(instance,uctx),None),
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 3e7479903a..30f716d764 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -117,9 +117,14 @@ let combine_appl appl1 appl2 =
let of_tacvalue v = in_gen (topwit wit_tacvalue) v
let to_tacvalue v = out_gen (topwit wit_tacvalue) v
+let log_trace = ref false
+
+let is_traced () =
+ !log_trace || !Flags.profile_ltac
+
(** More naming applications *)
let name_vfun appl vle =
- if has_type vle (topwit wit_tacvalue) then
+ if is_traced () && has_type vle (topwit wit_tacvalue) then
match to_tacvalue vle with
| VFun (appl0,trace,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,lfun,vars,t))
| _ -> vle
@@ -137,9 +142,11 @@ type interp_sign = Geninterp.interp_sign = {
lfun : value Id.Map.t;
extra : TacStore.t }
-let extract_trace ist = match TacStore.get ist.extra f_trace with
-| None -> []
-| Some l -> l
+let extract_trace ist =
+ if is_traced () then match TacStore.get ist.extra f_trace with
+ | None -> []
+ | Some l -> l
+ else []
let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
@@ -161,8 +168,11 @@ let catch_error call_trace f x =
let e = CErrors.push e in
catching_error call_trace iraise e
+let wrap_error tac k =
+ if is_traced () then Proofview.tclORELSE tac k else tac
+
let catch_error_tac call_trace tac =
- Proofview.tclORELSE
+ wrap_error
tac
(catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
@@ -203,9 +213,11 @@ let constr_of_id env id =
(** Generic arguments : table of interpretation functions *)
(* Some of the code further down depends on the fact that push_trace does not modify sigma (the evar map) *)
-let push_trace call ist = match TacStore.get ist.extra f_trace with
-| None -> Proofview.tclUNIT [call]
-| Some trace -> Proofview.tclUNIT (call :: trace)
+let push_trace call ist =
+ if is_traced () then match TacStore.get ist.extra f_trace with
+ | None -> Proofview.tclUNIT [call]
+ | Some trace -> Proofview.tclUNIT (call :: trace)
+ else Proofview.tclUNIT []
let propagate_trace ist loc id v =
if has_type v (topwit wit_tacvalue) then
@@ -530,7 +542,15 @@ let interp_gen kind ist pattern_mode flags env sigma c =
invariant that running the tactic returned by push_trace does
not modify sigma. *)
let (_, dummy_proofview) = Proofview.init sigma [] in
- let (trace,_,_,_) = Proofview.apply env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in
+
+ (* Again this is called at times with no open proof! *)
+ let name, poly =
+ try
+ let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in
+ name, poly
+ with | Proof_global.NoCurrentProof -> Id.of_string "tacinterp", false
+ in
+ let (trace,_,_,_) = Proofview.apply ~name ~poly env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in
let (evd,c) =
catch_error trace (understand_ltac flags env sigma vars kind) term
in
@@ -544,7 +564,9 @@ let constr_flags () = {
use_typeclasses = true;
solve_unification_constraints = true;
fail_evar = true;
- expand_evars = true }
+ expand_evars = true;
+ program_mode = false;
+}
(* Interprets a constr; expects evars to be solved *)
let interp_constr_gen kind ist env sigma c =
@@ -558,19 +580,25 @@ let open_constr_use_classes_flags () = {
use_typeclasses = true;
solve_unification_constraints = true;
fail_evar = false;
- expand_evars = true }
+ expand_evars = true;
+ program_mode = false;
+}
let open_constr_no_classes_flags () = {
use_typeclasses = false;
solve_unification_constraints = true;
fail_evar = false;
- expand_evars = true }
+ expand_evars = true;
+ program_mode = false;
+}
let pure_open_constr_flags = {
use_typeclasses = false;
solve_unification_constraints = true;
fail_evar = false;
- expand_evars = false }
+ expand_evars = false;
+ program_mode = false;
+}
(* Interprets an open constr *)
let interp_open_constr ?(expected_type=WithoutTypeConstraint) ?(flags=open_constr_no_classes_flags ()) ist env sigma c =
@@ -1247,7 +1275,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
let fold accu (id, v) = Id.Map.add id v accu in
let newlfun = List.fold_left fold olfun extfun in
if List.is_empty lvar then
- begin Proofview.tclORELSE
+ begin wrap_error
begin
let ist = {
lfun = newlfun;
@@ -1407,7 +1435,7 @@ and interp_match_successes lz ist s =
(* Interprets the Match expressions *)
and interp_match ist lz constr lmr =
let (>>=) = Ftactic.bind in
- begin Proofview.tclORELSE
+ begin wrap_error
(interp_ltac_constr ist constr)
begin function
| (e, info) ->
@@ -1493,7 +1521,7 @@ and interp_genarg_var_list ist x =
(* Interprets tactic expressions : returns a "constr" *)
and interp_ltac_constr ist e : EConstr.t Ftactic.t =
let (>>=) = Ftactic.bind in
- begin Proofview.tclORELSE
+ begin wrap_error
(val_interp ist e)
begin function (err, info) -> match err with
| Not_found ->
@@ -2033,7 +2061,16 @@ let _ =
let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
let ist = { lfun = lfun; extra; } in
let tac = interp_tactic ist tac in
- let name, poly = Id.of_string "ltac_sub", false in
+ (* XXX: This depends on the global state which is bad; the hooking
+ mechanism should be modified. *)
+ let name, poly =
+ try
+ let (_, poly, _) = Proof_global.get_current_persistence () in
+ let name = Proof_global.get_current_proof_name () in
+ name, poly
+ with | Proof_global.NoCurrentProof ->
+ Id.of_string "ltac_gen", false
+ in
let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in
(EConstr.of_constr c, sigma)
in
@@ -2051,4 +2088,13 @@ let () =
optread = (fun () -> get_debug () != Tactic_debug.DebugOff);
optwrite = vernac_debug }
+let () =
+ let open Goptions in
+ declare_bool_option
+ { optdepr = false;
+ optname = "Ltac Backtrace";
+ optkey = ["Ltac"; "Backtrace"];
+ optread = (fun () -> !log_trace);
+ optwrite = (fun b -> log_trace := b) }
+
let () = Hook.set Vernacentries.interp_redexp_hook interp_redexp
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 02:06:02 +0000