aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/g_ltac.mlg6
-rw-r--r--plugins/ltac/g_obligations.mlg2
-rw-r--r--plugins/ltac/g_rewrite.mlg2
-rw-r--r--plugins/ltac/leminv.ml3
-rw-r--r--plugins/ltac/pltac.ml36
-rw-r--r--plugins/ltac/pptactic.ml2
-rw-r--r--plugins/ltac/profile_ltac.ml4
-rw-r--r--plugins/ltac/rewrite.ml6
-rw-r--r--plugins/ltac/taccoerce.ml2
-rw-r--r--plugins/ltac/taccoerce.mli2
-rw-r--r--plugins/ltac/tacentries.ml2
-rw-r--r--plugins/ltac/tacinterp.ml59
12 files changed, 69 insertions, 57 deletions
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index ed14b6c748..6cf5d30a95 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -48,14 +48,14 @@ let reference_to_id qid =
CErrors.user_err ?loc:qid.CAst.loc
(str "This expression should be a simple identifier.")
-let tactic_mode = Entry.create "vernac:tactic_command"
+let tactic_mode = Entry.create "tactic_command"
let new_entry name =
let e = Entry.create name in
e
-let toplevel_selector = new_entry "vernac:toplevel_selector"
-let tacdef_body = new_entry "tactic:tacdef_body"
+let toplevel_selector = new_entry "toplevel_selector"
+let tacdef_body = new_entry "tacdef_body"
(* Registers [tactic_mode] as a parser for proof editing *)
let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index a6673699af..fc24475a62 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -56,7 +56,7 @@ type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_a
let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type =
Genarg.create_arg "withtac"
-let withtac = Pcoq.create_generic_entry Pcoq.utactic "withtac" (Genarg.rawwit wit_withtac)
+let withtac = Pcoq.create_generic_entry2 "withtac" (Genarg.rawwit wit_withtac)
}
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 09cdc997ab..8331927cda 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -219,7 +219,7 @@ type binders_argtype = local_binder_expr list
let wit_binders =
(Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type)
-let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wit_binders)
+let binders = Pcoq.create_generic_entry2 "binders" (Genarg.rawwit wit_binders)
let () =
let raw_printer env sigma _ _ _ l = Pp.pr_non_empty_arg (Ppconstr.pr_binders env sigma) l in
diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml
index 47df3ec34f..f42c1f73a3 100644
--- a/plugins/ltac/leminv.ml
+++ b/plugins/ltac/leminv.ml
@@ -245,7 +245,8 @@ let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
let add_inversion_lemma_exn ~poly na com comsort bool tac =
let env = Global.env () in
let sigma = Evd.from_env env in
- let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in
+ let c, uctx = Constrintern.interp_type env sigma com in
+ let sigma = Evd.from_ctx uctx in
let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in
add_inversion_lemma ~poly na env sigma c sort bool tac
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 5b5ee64a56..b7b54143df 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -11,39 +11,37 @@
open Pcoq
(* Main entry for extensions *)
-let simple_tactic = Entry.create "tactic:simple_tactic"
-
-let make_gen_entry _ name = Entry.create ("tactic:" ^ name)
+let simple_tactic = Entry.create "simple_tactic"
(* Typically for tactic user extensions *)
let open_constr =
- make_gen_entry utactic "open_constr"
+ Entry.create "open_constr"
let constr_with_bindings =
- make_gen_entry utactic "constr_with_bindings"
+ Entry.create "constr_with_bindings"
let bindings =
- make_gen_entry utactic "bindings"
+ Entry.create "bindings"
let hypident = Entry.create "hypident"
-let constr_may_eval = make_gen_entry utactic "constr_may_eval"
-let constr_eval = make_gen_entry utactic "constr_eval"
+let constr_may_eval = Entry.create "constr_may_eval"
+let constr_eval = Entry.create "constr_eval"
let uconstr =
- make_gen_entry utactic "uconstr"
+ Entry.create "uconstr"
let quantified_hypothesis =
- make_gen_entry utactic "quantified_hypothesis"
-let destruction_arg = make_gen_entry utactic "destruction_arg"
-let int_or_var = make_gen_entry utactic "int_or_var"
+ Entry.create "quantified_hypothesis"
+let destruction_arg = Entry.create "destruction_arg"
+let int_or_var = Entry.create "int_or_var"
let simple_intropattern =
- make_gen_entry utactic "simple_intropattern"
-let in_clause = make_gen_entry utactic "in_clause"
+ Entry.create "simple_intropattern"
+let in_clause = Entry.create "in_clause"
let clause_dft_concl =
- make_gen_entry utactic "clause"
+ Entry.create "clause"
(* Main entries for ltac *)
-let tactic_arg = Entry.create "tactic:tactic_arg"
-let tactic_expr = make_gen_entry utactic "tactic_expr"
-let binder_tactic = make_gen_entry utactic "binder_tactic"
+let tactic_arg = Entry.create "tactic_arg"
+let tactic_expr = Entry.create "tactic_expr"
+let binder_tactic = Entry.create "binder_tactic"
-let tactic = make_gen_entry utactic "tactic"
+let tactic = Entry.create "tactic"
(* Main entry for quotations *)
let tactic_eoi = eoi_entry tactic
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 85bb901046..cbb53497d3 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -179,7 +179,7 @@ let string_of_genarg_arg (ArgumentType arg) =
| ConstrTypeOf c ->
hov 1 (keyword "type of" ++ spc() ++ prc env sigma c)
| ConstrTerm c when test c ->
- h 0 (str "(" ++ prc env sigma c ++ str ")")
+ h (str "(" ++ prc env sigma c ++ str ")")
| ConstrTerm c ->
prc env sigma c
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 0dbf16a821..9c15d24dd3 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -146,7 +146,7 @@ let header =
fnl ()
let rec print_node ~filter all_total indent prefix (s, e) =
- h 0 (
+ h (
padr_with '-' 40 (prefix ^ s ^ " ")
++ padl 7 (format_ratio (e.local /. all_total))
++ padl 7 (format_ratio (e.total /. all_total))
@@ -212,7 +212,7 @@ let to_string ~filter ?(cutoff=0.0) node =
in
let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in
let msg =
- h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
+ h (str "total time: " ++ padl 11 (format_sec (all_total))) ++
fnl () ++
fnl () ++
header ++
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index a1dbf9a439..5ef76dbdc1 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -181,7 +181,7 @@ end) = struct
fun env sigma -> class_info env sigma (Lazy.force r)
let proper_proj env sigma =
- mkConst (Option.get (pi3 (List.hd (proper_class env sigma).cl_projs)))
+ mkConst (Option.get (List.hd (proper_class env sigma).cl_projs).meth_const)
let proper_type env (sigma,cstrs) =
let l = (proper_class env sigma).cl_impl in
@@ -498,7 +498,7 @@ let rec decompose_app_rel env evd t =
let decompose_app_rel env evd t =
let (rel, t1, t2) = decompose_app_rel env evd t in
- let ty = Retyping.get_type_of env evd rel in
+ let ty = try Retyping.get_type_of ~lax:true env evd rel with Retyping.RetypeError _ -> error_no_relation () in
let () = if not (Reductionops.is_arity env evd ty) then error_no_relation () in
(rel, t1, t2)
@@ -2144,7 +2144,7 @@ let setoid_proof ty fn fallback =
let car = snd (List.hd (fst (Reductionops.splay_prod env sigma t))) in
(try init_relation_classes () with _ -> raise Not_found);
fn env sigma car rel
- with e ->
+ with e when CErrors.noncritical e ->
(* XXX what is the right test here as to whether e can be converted ? *)
let e, info = Exninfo.capture e in
Proofview.tclZERO ~info e
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 91d26519b8..f7037176d2 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -394,7 +394,7 @@ type appl =
(* Values for interpretation *)
type tacvalue =
- | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t *
+ | VFun of appl * Tacexpr.ltac_trace * Loc.t option * Val.t Id.Map.t *
Name.t list * Tacexpr.glob_tactic_expr
| VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 3afbb56b23..b8592c5c76 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -104,7 +104,7 @@ type appl =
(** For calls to global constants, some may alias other. *)
type tacvalue =
- | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t *
+ | VFun of appl *Tacexpr.ltac_trace * Loc.t option * Val.t Id.Map.t *
Name.t list * Tacexpr.glob_tactic_expr
| VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index fcd60ea250..f0ca813b08 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -869,7 +869,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
let () = Pcoq.register_grammar wit e in
e
| Vernacextend.Arg_rules rules ->
- let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
+ let e = Pcoq.create_generic_entry2 name (Genarg.rawwit wit) in
let () = Pcoq.grammar_extend e {pos=None; data=[(None, None, rules)]} in
e
in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 54832f1068..eaeae50254 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -124,7 +124,7 @@ let is_traced () =
let name_vfun appl vle =
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))
+ | VFun (appl0,trace,loc,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,loc,lfun,vars,t))
| _ -> vle
else vle
@@ -134,6 +134,7 @@ let f_avoid_ids : Id.Set.t TacStore.field = TacStore.field ()
(* ids inherited from the call context (needed to get fresh ids) *)
let f_debug : debug_info TacStore.field = TacStore.field ()
let f_trace : ltac_trace TacStore.field = TacStore.field ()
+let f_loc : Loc.t TacStore.field = TacStore.field ()
(* Signature for interpretation: val_interp and interpretation functions *)
type interp_sign = Geninterp.interp_sign =
@@ -141,12 +142,23 @@ type interp_sign = Geninterp.interp_sign =
; poly : bool
; extra : TacStore.t }
+let add_extra_trace trace extra = TacStore.set extra f_trace trace
let extract_trace ist =
if is_traced () then match TacStore.get ist.extra f_trace with
| None -> []
| Some l -> l
else []
+let add_extra_loc loc extra =
+ match loc with
+ | None -> extra
+ | Some loc -> TacStore.set extra f_loc loc
+let add_loc loc ist =
+ match loc with
+ | None -> ist
+ | Some loc -> { ist with extra = TacStore.set ist.extra f_loc loc }
+let extract_loc ist = TacStore.get ist.extra f_loc
+
let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
let catching_error call_trace fail (e, info) =
@@ -222,7 +234,7 @@ let pr_inspect env expr result =
let pp_result =
if has_type result (topwit wit_tacvalue) then
match to_tacvalue result with
- | VFun (_,_, ist, ul, b) ->
+ | VFun (_, _, _, ist, ul, b) ->
let body = if List.is_empty ul then b else (TacFun (ul, b)) in
str "a closure with body " ++ fnl() ++ pr_closure env ist body
| VRec (ist, body) ->
@@ -249,10 +261,10 @@ let propagate_trace ist loc id v =
if has_type v (topwit wit_tacvalue) then
let tacv = to_tacvalue v in
match tacv with
- | VFun (appl,_,lfun,it,b) ->
+ | VFun (appl,_,_,lfun,it,b) ->
let t = if List.is_empty it then b else TacFun (it,b) in
let trace = push_trace(loc,LtacVarCall (id,t)) ist in
- let ans = VFun (appl,trace,lfun,it,b) in
+ let ans = VFun (appl,trace,loc,lfun,it,b) in
Proofview.tclUNIT (of_tacvalue ans)
| _ -> Proofview.tclUNIT v
else Proofview.tclUNIT v
@@ -260,7 +272,7 @@ let propagate_trace ist loc id v =
let append_trace trace v =
if has_type v (topwit wit_tacvalue) then
match to_tacvalue v with
- | VFun (appl,trace',lfun,it,b) -> of_tacvalue (VFun (appl,trace'@trace,lfun,it,b))
+ | VFun (appl,trace',loc,lfun,it,b) -> of_tacvalue (VFun (appl,trace'@trace,loc,lfun,it,b))
| _ -> v
else v
@@ -272,7 +284,7 @@ let coerce_to_tactic loc id v =
if has_type v (topwit wit_tacvalue) then
let tacv = to_tacvalue v in
match tacv with
- | VFun _ -> v
+ | VFun (appl,trace,_,lfun,it,b) -> of_tacvalue (VFun (appl,trace,loc,lfun,it,b))
| _ -> fail ()
else fail ()
@@ -1062,7 +1074,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
function. *)
let value_interp ist = match tac with
| TacFun (it, body) ->
- Ftactic.return (of_tacvalue (VFun (UnnamedAppl,extract_trace ist, ist.lfun, it, body)))
+ Ftactic.return (of_tacvalue (VFun (UnnamedAppl, extract_trace ist, extract_loc ist, ist.lfun, it, body)))
| TacLetIn (true,l,u) -> interp_letrec ist l u
| TacLetIn (false,l,u) -> interp_letin ist l u
| TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist lz lr lmr
@@ -1070,7 +1082,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
| TacArg {loc;v} -> interp_tacarg ist v
| t ->
(* Delayed evaluation *)
- Ftactic.return (of_tacvalue (VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], t)))
+ Ftactic.return (of_tacvalue (VFun (UnnamedAppl, extract_trace ist, extract_loc ist, ist.lfun, [], t)))
in
let open Ftactic in
Control.check_for_interrupt ();
@@ -1163,7 +1175,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with
| TacFirst l -> Tacticals.New.tclFIRST (List.map (interp_tactic ist) l)
| TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l)
| TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac)
- | TacArg a -> Ftactic.run (val_interp ist tac) (fun v -> catch_error_loc a.CAst.loc false (tactic_of_value ist v))
+ | TacArg {CAst.loc} -> Ftactic.run (val_interp (add_loc loc ist) tac) (fun v -> tactic_of_value ist v)
| TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
(* For extensions *)
| TacAlias {loc; v=(s,l)} ->
@@ -1178,9 +1190,9 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with
let ist = {
lfun
; poly
- ; extra = TacStore.set ist.extra f_trace trace } in
+ ; extra = add_extra_loc loc (add_extra_trace trace ist.extra) } in
val_interp ist alias.Tacenv.alias_body >>= fun v ->
- Ftactic.lift (catch_error_loc loc false (tactic_of_value ist v))
+ Ftactic.lift (tactic_of_value ist v)
in
let tac =
Ftactic.with_env interp_vars >>= fun (env, lr) ->
@@ -1243,7 +1255,8 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
let ist = { lfun = Id.Map.empty; poly; extra } in
let appl = GlbAppl[r,[]] in
Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false
- (catch_error_tac_loc loc false trace (val_interp ~appl ist (Tacenv.interp_ltac r)))
+ (catch_error_tac_loc (* interp *) loc false trace
+ (val_interp ~appl (add_loc (* exec *) loc ist) (Tacenv.interp_ltac r)))
and interp_tacarg ist arg : Val.t Ftactic.t =
match arg with
@@ -1297,8 +1310,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
is not a tactic that expects arguments.
Otherwise Ltac goes into an infinite loop (val_interp puts
a VFun back on body, and then interp_app is called again...) *)
- | (VFun(appl,trace,olfun,(_::_ as var),body)
- |VFun(appl,trace,olfun,([] as var),
+ | (VFun(appl,trace,_,olfun,(_::_ as var),body)
+ |VFun(appl,trace,_,olfun,([] as var),
(TacFun _|TacLetIn _|TacMatchGoal _|TacMatch _| TacArg _ as body))) ->
let (extfun,lvar,lval)=head_with_value (var,largs) in
let fold accu (id, v) = Id.Map.add id v accu in
@@ -1312,7 +1325,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
; extra = TacStore.set ist.extra f_trace []
} in
Profile_ltac.do_profile "interp_app" trace ~count_call:false
- (catch_error_tac_loc loc false trace (val_interp ist body)) >>= fun v ->
+ (catch_error_tac_loc loc false trace (val_interp (add_loc loc ist) body)) >>= fun v ->
Ftactic.return (name_vfun (push_appl appl largs) v)
end
begin fun (e, info) ->
@@ -1333,8 +1346,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
end <*>
if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval
else
- Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,newlfun,lvar,body)))
- | (VFun(appl,trace,olfun,[],body)) ->
+ Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,loc,newlfun,lvar,body)))
+ | (VFun(appl,trace,_,olfun,[],body)) ->
let extra_args = List.length largs in
let info = Exninfo.reify () in
Tacticals.New.tclZEROMSG ~info
@@ -1353,15 +1366,15 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
and tactic_of_value ist vle =
if has_type vle (topwit wit_tacvalue) then
match to_tacvalue vle with
- | VFun (appl,trace,lfun,[],t) ->
+ | VFun (appl,trace,loc,lfun,[],t) ->
Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
let ist = {
lfun = lfun;
poly;
extra = TacStore.set ist.extra f_trace []; } in
let tac = name_if_glob appl (eval_tactic_ist ist t) in
- Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac)
- | VFun (appl,_,vmap,vars,_) ->
+ Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac_loc loc false trace tac)
+ | VFun (appl,_,loc,vmap,vars,_) ->
let tactic_nm =
match appl with
UnnamedAppl -> "An unnamed user-defined tactic"
@@ -1440,14 +1453,14 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
let ist = { ist with lfun } in
val_interp ist lhs >>= fun v ->
if has_type v (topwit wit_tacvalue) then match to_tacvalue v with
- | VFun (appl,trace,lfun,[],t) ->
+ | VFun (appl,trace,loc,lfun,[],t) ->
let ist =
{ lfun = lfun
; poly
; extra = TacStore.set ist.extra f_trace trace
} in
let tac = eval_tactic_ist ist t in
- let dummy = VFun (appl,extract_trace ist, Id.Map.empty, [], TacId []) in
+ let dummy = VFun (appl, extract_trace ist, loc, Id.Map.empty, [], TacId []) in
catch_error_tac trace (tac <*> Ftactic.return (of_tacvalue dummy))
| _ -> Ftactic.return v
else Ftactic.return v
@@ -1940,7 +1953,7 @@ module Value = struct
include Taccoerce.Value
let of_closure ist tac =
- let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
+ let closure = VFun (UnnamedAppl, extract_trace ist, None, ist.lfun, [], tac) in
of_tacvalue closure
let apply_expr f args =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 20:16:17 +0000