aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ltac/coretactics.mlg2
-rw-r--r--plugins/ltac/extraargs.mlg2
-rw-r--r--plugins/ltac/g_ltac.mlg6
-rw-r--r--plugins/ltac/leminv.ml17
-rw-r--r--plugins/ltac/pptactic.ml11
-rw-r--r--plugins/ltac/taccoerce.ml2
-rw-r--r--plugins/ltac/taccoerce.mli2
-rw-r--r--plugins/ltac/tacentries.ml8
-rw-r--r--plugins/ltac/tacexpr.ml2
-rw-r--r--plugins/ltac/tacexpr.mli2
-rw-r--r--plugins/ltac/tacintern.ml6
-rw-r--r--plugins/ltac/tacinterp.ml61
-rw-r--r--plugins/ltac/tacsubst.ml2
-rw-r--r--plugins/micromega/dune2
-rw-r--r--plugins/setoid_ring/newring.ml6
-rw-r--r--plugins/ssr/ssrparser.mlg8
16 files changed, 75 insertions, 64 deletions
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index cb226de586..f1f538ab39 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -263,7 +263,7 @@ END
(** Double induction *)
-TACTIC EXTEND double_induction
+TACTIC EXTEND double_induction DEPRECATED { Deprecation.make () }
| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
{ Elim.h_double_induction h1 h2 }
END
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index eb53fd45d0..863c4d37d8 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -25,7 +25,7 @@ open Locus
(** Adding scopes for generic arguments not defined through ARGUMENT EXTEND *)
let create_generic_quotation name e wit =
- let inject (loc, v) = Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v) in
+ let inject (loc, v) = Tacexpr.TacGeneric (Some name, Genarg.in_gen (Genarg.rawwit wit) v) in
Tacentries.create_ltac_quotation name inject (e, None)
let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 78cde2cde8..d88cda177e 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -180,7 +180,7 @@ GRAMMAR EXTEND Gram
[ [ a = tactic_arg -> { a }
| c = Constr.constr -> { (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) }
(* Unambiguous entries: tolerated w/o "ltac:" modifier *)
- | "()" -> { TacGeneric (genarg_of_unit ()) } ] ]
+ | "()" -> { TacGeneric (None, genarg_of_unit ()) } ] ]
;
(* Can be used as argument and at toplevel in tactic expressions. *)
tactic_arg:
@@ -209,9 +209,9 @@ GRAMMAR EXTEND Gram
| c = Constr.constr -> { ConstrTerm c } ] ]
;
tactic_atom:
- [ [ n = integer -> { TacGeneric (genarg_of_int n) }
+ [ [ n = integer -> { TacGeneric (None, genarg_of_int n) }
| r = reference -> { TacCall (CAst.make ~loc (r,[])) }
- | "()" -> { TacGeneric (genarg_of_unit ()) } ] ]
+ | "()" -> { TacGeneric (None, genarg_of_unit ()) } ] ]
;
match_key:
[ [ "match" -> { Once }
diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml
index 0024d1a4ba..47df3ec34f 100644
--- a/plugins/ltac/leminv.ml
+++ b/plugins/ltac/leminv.ml
@@ -228,14 +228,15 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
let c = fill_holes pfterm in
(* warning: side-effect on ownSign *)
let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
- let p = EConstr.to_constr sigma invProof in
- p, sigma
+ invProof, sigma
let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in
- let univs = Evd.univ_entry ~poly sigma in
- let entry = Declare.definition_entry ~univs invProof in
- let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Lemma) (Declare.DefinitionEntry entry) in
+ let cinfo = Declare.CInfo.make ~name ~typ:None () in
+ let info = Declare.Info.make ~poly ~kind:Decls.(IsProof Lemma) () in
+ let _ : Names.GlobRef.t =
+ Declare.declare_definition ~cinfo ~info ~opaque:false ~body:invProof sigma
+ in
()
(* inv_op = Inv (derives de complete inv. lemma)
@@ -246,11 +247,7 @@ let add_inversion_lemma_exn ~poly na com comsort bool tac =
let sigma = Evd.from_env env in
let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in
let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in
- try
- add_inversion_lemma ~poly na env sigma c sort bool tac
- with
- | UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
- user_err ~hdr:"Inv needs Nodep Prop Set" s
+ add_inversion_lemma ~poly na env sigma c sort bool tac
(* ================================= *)
(* Applying a given inversion lemma *)
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index f69fe064a7..85bb901046 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -338,8 +338,8 @@ let string_of_genarg_arg (ArgumentType arg) =
| Extend.Uentryl (_, l) -> prtac LevelSome arg
| _ ->
match arg with
- | TacGeneric arg ->
- let pr l arg = prtac l (TacGeneric arg) in
+ | TacGeneric (isquot,arg) ->
+ let pr l arg = prtac l (TacGeneric (isquot,arg)) in
pr_any_arg pr symb arg
| _ -> str "ltac:(" ++ prtac LevelSome arg ++ str ")"
@@ -571,7 +571,7 @@ let pr_goal_selector ~toplevel s =
let pr_let_clause k pr_gen pr_arg (na,(bl,t)) =
let pr = function
- | TacGeneric arg ->
+ | TacGeneric (_,arg) ->
let name = string_of_genarg_arg (genarg_tag arg) in
if name = "unit" || name = "int" then
(* Hard-wired parsing rules *)
@@ -1049,8 +1049,9 @@ let pr_goal_selector ~toplevel s =
pr_may_eval env sigma pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval
| TacArg { CAst.v=TacFreshId l } ->
primitive "fresh" ++ pr_fresh_ids l, latom
- | TacArg { CAst.v=TacGeneric arg } ->
- pr.pr_generic env sigma arg, latom
+ | TacArg { CAst.v=TacGeneric (isquot,arg) } ->
+ let p = pr.pr_generic env sigma arg in
+ (match isquot with Some name -> str name ++ str ":(" ++ p ++ str ")" | None -> p), latom
| TacArg { CAst.v=TacCall {CAst.v=(f,[])} } ->
pr.pr_reference f, latom
| TacArg { CAst.v=TacCall {CAst.loc; v=(f,l)} } ->
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 f8c25d5dd0..fcd60ea250 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -174,7 +174,7 @@ let add_tactic_entry (kn, ml, tg) state =
if Genarg.has_type arg wit && not ml then
Tacexp (Genarg.out_gen wit arg)
else
- TacGeneric arg
+ TacGeneric (None, arg)
in
let l = List.map map l in
(TacAlias (CAst.make ~loc (kn,l)):raw_tactic_expr)
@@ -349,7 +349,7 @@ let extend_atomic_tactic name entries =
| TacNonTerm (_, (symb, _)) ->
let EntryName (typ, e) = prod_item_of_symbol 0 symb in
let Genarg.Rawwit wit = typ in
- let inj x = TacArg (CAst.make @@ TacGeneric (Genarg.in_gen typ x)) in
+ let inj x = TacArg (CAst.make @@ TacGeneric (None, Genarg.in_gen typ x)) in
let default = epsilon_value inj e in
match default with
| None -> raise NonEmptyArgument
@@ -780,7 +780,7 @@ let ml_val_tactic_extend ~plugin ~name ~local ?deprecation sign tac =
let ml_tactic_name = { mltac_tactic = name; mltac_plugin = plugin } in
let len = ml_sig_len sign in
let vars = List.init len (fun i -> Id.of_string (Printf.sprintf "arg%i" i)) in
- let body = TacGeneric (in_tacval { tacval_tac = ml_tactic_name; tacval_var = vars }) in
+ let body = TacGeneric (None, in_tacval { tacval_tac = ml_tactic_name; tacval_var = vars }) in
let vars = List.map (fun id -> Name id) vars in
let body = Tacexpr.TacFun (vars, Tacexpr.TacArg (CAst.make body)) in
let id = Names.Id.of_string name in
@@ -876,7 +876,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
let (rpr, gpr, tpr) = arg.arg_printer in
let () = Pptactic.declare_extra_genarg_pprule wit rpr gpr tpr in
let () = create_ltac_quotation name
- (fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v))
+ (fun (loc, v) -> Tacexpr.TacGeneric (Some name,Genarg.in_gen (Genarg.rawwit wit) v))
(entry, None)
in
(wit, entry)
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index b261096b63..eaedf8d9c1 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -154,7 +154,7 @@ constraint 'a = <
(** Possible arguments of a tactic definition *)
type 'a gen_tactic_arg =
- | TacGeneric of 'lev generic_argument
+ | TacGeneric of string option * 'lev generic_argument
| ConstrMayEval of ('trm,'cst,'pat) may_eval
| Reference of 'ref
| TacCall of ('ref * 'a gen_tactic_arg list) CAst.t
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 650349b586..50767821e4 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -153,7 +153,7 @@ constraint 'a = <
(** Possible arguments of a tactic definition *)
type 'a gen_tactic_arg =
- | TacGeneric of 'lev generic_argument
+ | TacGeneric of string option * 'lev generic_argument
| ConstrMayEval of ('trm,'cst,'pat) may_eval
| Reference of 'ref
| TacCall of ('ref * 'a gen_tactic_arg list) CAst.t
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index afa79a88db..dea216045e 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -195,7 +195,7 @@ let intern_non_tactic_reference strict ist qid =
if qualid_is_ident qid && not strict then
let id = qualid_basename qid in
let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc:qid.CAst.loc @@ IntroNaming (IntroIdentifier id)) in
- TacGeneric ipat
+ TacGeneric (None,ipat)
else
(* Reference not found *)
let _, info = Exninfo.capture exn in
@@ -713,9 +713,9 @@ and intern_tacarg strict onlytac ist = function
| TacPretype c -> TacPretype (intern_constr ist c)
| TacNumgoals -> TacNumgoals
| Tacexp t -> Tacexp (intern_tactic onlytac ist t)
- | TacGeneric arg ->
+ | TacGeneric (isquot,arg) ->
let arg = intern_genarg ist arg in
- TacGeneric arg
+ TacGeneric (isquot,arg)
(* Reads the rules of a Match Context or a Match *)
and intern_match_rule onlytac ist ?(as_type=false) = function
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 2258201c22..ff6a36a049 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,11 +1255,12 @@ 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
- | TacGeneric arg -> interp_genarg ist arg
+ | TacGeneric (_,arg) -> interp_genarg ist arg
| Reference r -> interp_ltac_reference false ist r
| ConstrMayEval c ->
Ftactic.enter begin fun gl ->
@@ -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 =
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index c2f1589b74..fd869b225f 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -237,7 +237,7 @@ and subst_tacarg subst = function
| TacPretype c -> TacPretype (subst_glob_constr subst c)
| TacNumgoals -> TacNumgoals
| Tacexp t -> Tacexp (subst_tactic subst t)
- | TacGeneric arg -> TacGeneric (subst_genarg subst arg)
+ | TacGeneric (isquot,arg) -> TacGeneric (isquot,subst_genarg subst arg)
(* Reads the rules of a Match Context or a Match *)
and subst_match_rule subst = function
diff --git a/plugins/micromega/dune b/plugins/micromega/dune
index 33ad3a0138..204125ab56 100644
--- a/plugins/micromega/dune
+++ b/plugins/micromega/dune
@@ -4,7 +4,7 @@
; be careful not to link the executable to the plugin!
(modules (:standard \ csdpcert g_zify zify))
(synopsis "Coq's micromega plugin")
- (libraries num coq.plugins.ltac))
+ (libraries coq.plugins.ltac))
(executable
(name csdpcert)
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 6ed6b8da91..5f5a974b6a 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -127,8 +127,8 @@ let closed_term_ast =
let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in
TacFun([Name(Id.of_string"t")],
TacML(CAst.make (tacname,
- [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.make @@ GVar(Id.of_string"t"),None));
- TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)])))
+ [TacGeneric (None, Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.make @@ GVar(Id.of_string"t"),None));
+ TacGeneric (None, Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)])))
(*
let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
*)
@@ -200,7 +200,7 @@ let exec_tactic env evd n f args =
(* Build the getter *)
let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in
let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in
- let get_res = TacML (CAst.make (get_res, [TacGeneric n])) in
+ let get_res = TacML (CAst.make (get_res, [TacGeneric (None, n)])) in
let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in
(* Evaluate the whole result *)
let gl = dummy_goal env evd in
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 98439e27a1..b32b58062a 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -1682,7 +1682,7 @@ let set_pr_ssrtac name prec afmt = (* FIXME *) () (*
let ssrtac_expr ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name, args))
let tclintros_expr ?loc tac ipats =
- let args = [Tacexpr.TacGeneric (in_gen (rawwit wit_ssrintrosarg) (tac, ipats))] in
+ let args = [Tacexpr.TacGeneric (None, in_gen (rawwit wit_ssrintrosarg) (tac, ipats))] in
ssrtac_expr ?loc "tclintros" args
}
@@ -1777,7 +1777,7 @@ let _ = set_pr_ssrtac "tcldo" 3 [ArgSep "do "; ArgSsr "doarg"]
let ssrdotac_expr ?loc n m tac clauses =
let arg = ((n, m), tac), clauses in
- ssrtac_expr ?loc "tcldo" [Tacexpr.TacGeneric (in_gen (rawwit wit_ssrdoarg) arg)]
+ ssrtac_expr ?loc "tcldo" [Tacexpr.TacGeneric (None, in_gen (rawwit wit_ssrdoarg) arg)]
}
@@ -1828,7 +1828,7 @@ let tclseq_expr ?loc tac dir arg =
let arg1 = in_gen (rawwit wit_ssrtclarg) tac in
let arg2 = in_gen (rawwit wit_ssrseqdir) dir in
let arg3 = in_gen (rawwit wit_ssrseqarg) (check_seqtacarg dir arg) in
- ssrtac_expr ?loc "tclseq" (List.map (fun x -> Tacexpr.TacGeneric x) [arg1; arg2; arg3])
+ ssrtac_expr ?loc "tclseq" (List.map (fun x -> Tacexpr.TacGeneric (None, x)) [arg1; arg2; arg3])
}
@@ -2451,7 +2451,7 @@ GRAMMAR EXTEND Gram
tactic_expr: LEVEL "3"
[ RIGHTA [ IDENT "abstract"; gens = ssrdgens ->
{ ssrtac_expr ~loc "abstract"
- [Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]];
+ [Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]];
END
TACTIC EXTEND ssrabstract
| [ "abstract" ssrdgens(gens) ] -> {
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 03:08:11 +0000