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/g_ltac.mlg11
-rw-r--r--plugins/ltac/g_obligations.mlg2
-rw-r--r--plugins/ltac/g_rewrite.mlg4
-rw-r--r--plugins/ltac/g_tactic.mlg8
-rw-r--r--plugins/ltac/rewrite.ml6
-rw-r--r--plugins/ltac/tacinterp.ml80
8 files changed, 83 insertions, 38 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/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index d9b19c1ae6..4c24f51b1e 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -58,15 +58,8 @@ let new_entry name =
let toplevel_selector = new_entry "vernac:toplevel_selector"
let tacdef_body = new_entry "tactic:tacdef_body"
-(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
- proof editing and changes nothing else). Then sets it as the default proof mode. *)
-let _ =
- let mode = {
- Proof_global.name = "Classic";
- set = (fun () -> Pvernac.set_command_entry tactic_mode);
- reset = (fun () -> Pvernac.(set_command_entry noedit_mode));
- } in
- Proof_global.register_proof_mode mode
+(* Registers [tactic_mode] as a parser for proof editing *)
+let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode
(* Hack to parse "[ id" without dropping [ *)
let test_bracket_ident =
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 1ea6ff84d4..cdee012a82 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -83,7 +83,7 @@ open Obligations
let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac
let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac
-let classify_obbl _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater)
+let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater)
}
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 31fb1c9abf..db8d1b20d8 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -285,13 +285,13 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
add_morphism_infer atts m n;
}
| #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
- => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater }
+ => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
-> {
add_morphism atts [] m s n;
}
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
"with" "signature" lconstr(s) "as" ident(n) ]
- => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater }
+ => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
-> {
add_morphism atts binders m s n;
}
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 46ea3819ac..7bf705ffeb 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -287,10 +287,10 @@ GRAMMAR EXTEND Gram
[ [ c = smart_global; nl = occs -> { (nl,c) } ] ]
;
intropatterns:
- [ [ l = LIST0 nonsimple_intropattern -> { l } ] ]
+ [ [ l = LIST0 intropattern -> { l } ] ]
;
ne_intropatterns:
- [ [ l = LIST1 nonsimple_intropattern -> { l } ] ]
+ [ [ l = LIST1 intropattern -> { l } ] ]
;
or_and_intropattern:
[ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> { IntroOrPattern tc }
@@ -317,7 +317,7 @@ GRAMMAR EXTEND Gram
| "?" -> { IntroAnonymous }
| id = ident -> { IntroIdentifier id } ] ]
;
- nonsimple_intropattern:
+ intropattern:
[ [ l = simple_intropattern -> { l }
| "*" -> { CAst.make ~loc @@ IntroForthcoming true }
| "**" -> { CAst.make ~loc @@ IntroForthcoming false } ] ]
@@ -534,6 +534,8 @@ GRAMMAR EXTEND Gram
{ TacAtom (CAst.make ~loc @@ TacIntroPattern (false,[CAst.make ~loc @@IntroForthcoming false])) }
| IDENT "eintros"; pl = ne_intropatterns ->
{ TacAtom (CAst.make ~loc @@ TacIntroPattern (true,pl)) }
+ | IDENT "eintros" ->
+ { TacAtom (CAst.make ~loc @@ TacIntroPattern (true,[CAst.make ~loc @@IntroForthcoming false])) }
| IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
inhyp = in_hyp_as -> { TacAtom (CAst.make ~loc @@ TacApply (true,false,cl,inhyp)) }
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 4bb52f599a..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),
@@ -2014,7 +2014,7 @@ let add_morphism atts binders m s n =
in
let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
ignore(new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance
- (Some (true, CAst.make @@ CRecord []))
+ None
~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
(** Bind to "rewrite" too *)
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-04 18:16:33 +0000