aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/coretactics.mlg7
-rw-r--r--plugins/ltac/extratactics.mlg26
-rw-r--r--plugins/ltac/g_auto.mlg15
-rw-r--r--plugins/ltac/g_ltac.mlg2
-rw-r--r--plugins/ltac/g_obligations.mlg8
-rw-r--r--plugins/ltac/g_tactic.mlg8
-rw-r--r--plugins/ltac/pltac.ml2
-rw-r--r--plugins/ltac/pltac.mli1
-rw-r--r--plugins/ltac/pptactic.ml8
-rw-r--r--plugins/ltac/pptactic.mli2
-rw-r--r--plugins/ltac/profile_ltac.ml6
-rw-r--r--plugins/ltac/rewrite.ml49
-rw-r--r--plugins/ltac/taccoerce.ml13
-rw-r--r--plugins/ltac/taccoerce.mli2
-rw-r--r--plugins/ltac/tacexpr.ml4
-rw-r--r--plugins/ltac/tacexpr.mli4
-rw-r--r--plugins/ltac/tacintern.ml4
-rw-r--r--plugins/ltac/tacsubst.ml2
-rw-r--r--plugins/ltac/tauto.ml1
19 files changed, 78 insertions, 86 deletions
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index e39c066c95..b20c4d173d 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -259,13 +259,6 @@ TACTIC EXTEND simple_destruct
| [ "simple" "destruct" quantified_hypothesis(h) ] -> { simple_destruct h }
END
-(** Double induction *)
-
-TACTIC EXTEND double_induction DEPRECATED { Deprecation.make () }
-| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
- { Elim.h_double_induction h1 h2 }
-END
-
(* Admit *)
TACTIC EXTEND admit
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 0b5d36b845..d9da47134d 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -299,7 +299,7 @@ TACTIC EXTEND rewrite_star
{
-let add_rewrite_hint ~poly bases ort t lcsr =
+let add_rewrite_hint ~locality ~poly bases ort t lcsr =
let env = Global.env() in
let sigma = Evd.from_env env in
let f ce =
@@ -315,7 +315,7 @@ let add_rewrite_hint ~poly bases ort t lcsr =
in
CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
let eqs = List.map f lcsr in
- let add_hints base = add_rew_rules base eqs in
+ let add_hints base = add_rew_rules ~locality base eqs in
List.iter add_hints bases
let classify_hint _ = VtSideff ([], VtLater)
@@ -323,15 +323,15 @@ let classify_hint _ = VtSideff ([], VtLater)
}
VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY { classify_hint }
-| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
- { add_rewrite_hint ~poly:polymorphic bl o None l }
-| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
+| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
+ { add_rewrite_hint ~locality ~poly:polymorphic bl o None l }
+| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
":" preident_list(bl) ] ->
- { add_rewrite_hint ~poly:polymorphic bl o (Some t) l }
-| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
- { add_rewrite_hint ~poly:polymorphic ["core"] o None l }
-| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
- { add_rewrite_hint ~poly:polymorphic ["core"] o (Some t) l }
+ { add_rewrite_hint ~locality ~poly:polymorphic bl o (Some t) l }
+| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
+ { add_rewrite_hint ~locality ~poly:polymorphic ["core"] o None l }
+| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
+ { add_rewrite_hint ~locality ~poly:polymorphic ["core"] o (Some t) l }
END
(**********************************************************************)
@@ -608,7 +608,7 @@ END
{
let subst_var_with_hole occ tid t =
- let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in
+ let occref = if occ > 0 then ref occ else Locusops.error_invalid_occurrence [occ] in
let locref = ref 0 in
let rec substrec x = match DAst.get x with
| GVar id ->
@@ -628,7 +628,7 @@ let subst_var_with_hole occ tid t =
| _ -> map_glob_constr_left_to_right substrec x in
let t' = substrec t
in
- if !occref > 0 then Find_subterm.error_invalid_occurrence [occ] else t'
+ if !occref > 0 then Locusops.error_invalid_occurrence [occ] else t'
let subst_hole_with_term occ tc t =
let locref = ref 0 in
@@ -774,7 +774,7 @@ let rec find_a_destructable_match sigma t =
let cl = [cl, (None, None), None], None in
let dest = TacAtom (CAst.make @@ TacInductionDestruct(false, false, cl)) in
match EConstr.kind sigma t with
- | Case (_,_,_,x,_) when closed0 sigma x ->
+ | Case (_,_,_,_,_,x,_) when closed0 sigma x ->
if isVar sigma x then
(* TODO check there is no rel n. *)
raise (Found (Tacinterp.eval_tactic dest))
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 069a342b2a..82b41e41bd 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -11,7 +11,6 @@
{
open Pp
-open Constr
open Stdarg
open Pcoq.Prim
open Pcoq.Constr
@@ -199,20 +198,6 @@ TACTIC EXTEND unify
END
{
-let deprecated_convert_concl_no_check =
- CWarnings.create
- ~name:"convert_concl_no_check" ~category:"deprecated"
- (fun () -> Pp.str "The syntax [convert_concl_no_check] is deprecated. Use [change_no_check] instead.")
-}
-
-TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> {
- deprecated_convert_concl_no_check ();
- Tactics.convert_concl ~check:false x DEFAULTcast
- }
-END
-
-{
let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid
let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index b1b96ea9a7..3da5b2bfc4 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -147,7 +147,7 @@ GRAMMAR EXTEND Gram
| IDENT "solve" ; "["; l = LIST0 ltac_expr SEP "|"; "]" ->
{ TacSolve l }
| IDENT "idtac"; l = LIST0 message_token -> { TacId l }
- | g=failkw; n = [ n = int_or_var -> { n } | -> { fail_default_value } ];
+ | g=failkw; n = [ n = nat_or_var -> { n } | -> { fail_default_value } ];
l = LIST0 message_token -> { TacFail (g,n,l) }
| st = simple_tactic -> { st }
| a = tactic_value -> { TacArg(CAst.make ~loc a) }
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 6bf330c830..e7902d06eb 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -151,13 +151,13 @@ VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
END
VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY STATE read_program
-| [ "Obligations" "of" ident(name) ] -> { show_obligations (Some name) }
-| [ "Obligations" ] -> { show_obligations None }
+| [ "Obligations" "of" ident(name) ] -> { fun ~stack:_ -> show_obligations (Some name) }
+| [ "Obligations" ] -> { fun ~stack:_ -> show_obligations None }
END
VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY STATE read_program
-| [ "Preterm" "of" ident(name) ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm (Some name)) }
-| [ "Preterm" ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm None) }
+| [ "Preterm" "of" ident(name) ] -> { fun ~stack:_ ~pm -> Feedback.msg_notice (show_term ~pm (Some name)) }
+| [ "Preterm" ] -> { fun ~stack:_ ~pm -> Feedback.msg_notice (show_term ~pm None) }
END
{
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 43957bbde5..cb430efb40 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -182,6 +182,11 @@ let merge_occurrences loc cl = function
in
(Some p, ans)
+let deprecated_conversion_at_with =
+ CWarnings.create
+ ~name:"conversion_at_with" ~category:"deprecated"
+ (fun () -> Pp.str "The syntax [at ... with ...] is deprecated. Use [with ... at ...] instead.")
+
(* Auxiliary grammar rules *)
open Pvernac.Vernac_
@@ -230,7 +235,8 @@ GRAMMAR EXTEND Gram
[ [ c = constr -> { (None, c) }
| c1 = constr; "with"; c2 = constr -> { (Some (AllOccurrences,c1),c2) }
| c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr ->
- { (Some (occs,c1), c2) } ] ]
+ { deprecated_conversion_at_with (); (* 8.14 *)
+ (Some (occs,c1), c2) } ] ]
;
occs_nums:
[ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl }
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 80c13a3698..196a68e67c 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -47,6 +47,8 @@ let binder_tactic = Entry.create "binder_tactic"
let tactic = Entry.create "tactic"
(* Main entry for quotations *)
+let tactic_eoi = eoi_entry tactic
+
let () =
let open Stdarg in
let open Tacarg in
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 73bce84d18..c0bf6b9f76 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -40,3 +40,4 @@ val tactic_expr : raw_tactic_expr Entry.t
[@@deprecated "Deprecated in 8.13; use 'ltac_expr' instead"]
val binder_tactic : raw_tactic_expr Entry.t
val tactic : raw_tactic_expr Entry.t
+val tactic_eoi : raw_tactic_expr Entry.t
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index faad792ea9..6ebb01703f 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -191,8 +191,8 @@ let string_of_genarg_arg (ArgumentType arg) =
let pr_and_short_name pr (c,_) = pr c
let pr_evaluable_reference = function
- | EvalVarRef id -> pr_id id
- | EvalConstRef sp -> pr_global (GlobRef.ConstRef sp)
+ | Tacred.EvalVarRef id -> pr_id id
+ | Tacred.EvalConstRef sp -> pr_global (GlobRef.ConstRef sp)
let pr_quantified_hypothesis = function
| AnonHyp n -> int n
@@ -381,8 +381,8 @@ let string_of_genarg_arg (ArgumentType arg) =
str "<" ++ KerName.print kn ++ str ">"
let pr_evaluable_reference_env env = function
- | EvalVarRef id -> pr_id id
- | EvalConstRef sp ->
+ | Tacred.EvalVarRef id -> pr_id id
+ | Tacred.EvalConstRef sp ->
Nametab.pr_global_env (Termops.vars_of_env env) (GlobRef.ConstRef sp)
let pr_as_disjunctive_ipat prc ipatl =
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 79e0adf9f7..4f58eceb59 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -106,7 +106,7 @@ val pr_may_eval :
val pr_and_short_name : ('a -> Pp.t) -> 'a Genredexpr.and_short_name -> Pp.t
-val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t
+val pr_evaluable_reference_env : env -> Tacred.evaluable_global_reference -> Pp.t
val pr_quantified_hypothesis : quantified_hypothesis -> Pp.t
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index aa2449d962..937d579012 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -436,11 +436,7 @@ let finish_timing ~prefix name =
(* ******************** *)
let print_results_filter ~cutoff ~filter =
- (* The STM doesn't provide yet a proper document query and traversal
- API, thus we need to re-check if some states are current anymore
- (due to backtracking) using the `state_of_id` API. *)
- let valid (did,id) _ = Stm.(state_of_id ~doc:(get_doc did) id) <> `Expired in
- data := SM.filter valid !data;
+ data := SM.filter (fun (doc,id) _ -> Stateid.is_valid ~doc id) !data;
let results =
SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
let results = merge_roots results Local.(CList.last !stack) in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 77162ce89a..6d0e0c36b3 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -855,26 +855,20 @@ let coerce env cstr res =
let res = { res with rew_evars = evars } in
apply_constraint env res.rew_car rel prf cstr res
-let apply_rule unify loccs : int pure_strategy =
- let (nowhere_except_in,occs) = convert_occs loccs in
- let is_occ occ =
- if nowhere_except_in
- then List.mem occ occs
- else not (List.mem occ occs)
- in
- { strategy = fun { state = occ ; env ;
+let apply_rule unify : occurrences_count pure_strategy =
+ { strategy = fun { state = occs ; env ;
term1 = t ; ty1 = ty ; cstr ; evars } ->
let unif = if isEvar (goalevars evars) t then None else unify env evars t in
match unif with
- | None -> (occ, Fail)
+ | None -> (occs, Fail)
| Some rew ->
- let occ = succ occ in
- if not (is_occ occ) then (occ, Fail)
- else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity)
+ let b, occs = update_occurrence_counter occs in
+ if not b then (occs, Fail)
+ else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occs, Identity)
else
let res = { rew with rew_car = ty } in
let res = Success (coerce env cstr res) in
- (occ, res)
+ (occs, res)
}
let apply_lemma l2r flags oc by loccs : strategy = { strategy =
@@ -890,9 +884,10 @@ let apply_lemma l2r flags oc by loccs : strategy = { strategy =
| None -> None
| Some rew -> Some rew
in
- let _, res = (apply_rule unify loccs).strategy { input with
- state = 0 ;
+ let loccs, res = (apply_rule unify).strategy { input with
+ state = initialize_occurrence_counter loccs ;
evars } in
+ check_used_occurrences loccs;
(), res
}
@@ -923,7 +918,8 @@ let reset_env env =
Environ.push_rel_context (Environ.rel_context env) env'
let fold_match ?(force=false) env sigma c =
- let (ci, p, iv, c, brs) = destCase sigma c in
+ let case = destCase sigma c in
+ let (ci, p, iv, c, brs) = EConstr.expand_case env sigma case in
let cty = Retyping.get_type_of env sigma c in
let dep, pred, exists, sk =
let env', ctx, body =
@@ -991,7 +987,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let argty = Retyping.get_type_of env (goalevars evars) arg in
let state, res = s.strategy { state ; env ;
unfresh ;
- term1 = arg ; ty1 = argty ;
+ term1 = arg ; ty1 = argty ;
cstr = (prop,None) ;
evars } in
let res' =
@@ -1158,7 +1154,8 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| Fail | Identity -> b'
in state, res
- | Case (ci, p, iv, c, brs) ->
+ | Case (ci, u, pms, p, iv, c, brs) ->
+ let (ci, p, iv, c, brs) = EConstr.expand_case env (goalevars evars) (ci, u, pms, p, iv, c, brs) in
let cty = Retyping.get_type_of env (goalevars evars) c in
let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in
let cstr' = Some eqty in
@@ -1168,7 +1165,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let state, res =
match c' with
| Success r ->
- let case = mkCase (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs) in
+ let case = mkCase (EConstr.contract_case env (goalevars evars) (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs)) in
let res = make_leibniz_proof env case ty r in
state, Success (coerce env (prop,cstr) res)
| Fail | Identity ->
@@ -1190,7 +1187,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
in
match found with
| Some r ->
- let ctxc = mkCase (ci, lift 1 p, map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c'))) in
+ let ctxc = mkCase (EConstr.contract_case env (goalevars evars) (ci, lift 1 p, map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c')))) in
state, Success (make_leibniz_proof env ctxc ty r)
| None -> state, c'
else
@@ -1391,7 +1388,7 @@ module Strategies =
let fold_glob c : 'a pure_strategy = { strategy =
fun { state ; env ; term1 = t ; ty1 = ty ; cstr ; evars } ->
-(* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
+(* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
let unfolded =
try Tacred.try_red_product env sigma c
@@ -1423,12 +1420,13 @@ let rewrite_with l2r flags c occs : strategy = { strategy =
let (sigma, rew) = refresh_hypinfo env sigma c in
unify_eqn rew l2r flags env (sigma, cstrs) None t
in
- let app = apply_rule unify occs in
+ let app = apply_rule unify in
let strat =
Strategies.fix (fun aux ->
Strategies.choice app (subterm true default_flags aux))
in
- let _, res = strat.strategy { input with state = 0 } in
+ let occs, res = strat.strategy { input with state = initialize_occurrence_counter occs } in
+ check_used_occurrences occs;
((), res)
}
@@ -2076,11 +2074,12 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals =
Proofview.Goal.enter begin fun gl ->
let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in
let unify env evars t = unify_abs res l2r sort env evars t in
- let app = apply_rule unify occs in
+ let app = apply_rule unify in
let recstrat aux = Strategies.choice app (subterm true general_rewrite_flags aux) in
let substrat = Strategies.fix recstrat in
let strat = { strategy = fun ({ state = () } as input) ->
- let _, res = substrat.strategy { input with state = 0 } in
+ let occs, res = substrat.strategy { input with state = initialize_occurrence_counter occs } in
+ check_used_occurrences occs;
(), res
}
in
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 4c1fe6417e..5e88bf7c79 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -276,6 +276,7 @@ let coerce_to_closed_constr env v =
c
let coerce_to_evaluable_ref env sigma v =
+ let open Tacred in
let fail () = raise (CannotCoerceTo "an evaluable reference") in
let ev =
match is_intro_pattern v with
@@ -429,7 +430,15 @@ let pr_value env v =
| TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } ->
pr_with_env (fun env sigma -> printer env sigma default_already_surrounded)
-let error_ltac_variable ?loc id env v s =
- CErrors.user_err ?loc (str "Ltac variable " ++ Id.print id ++
+exception CoercionError of Id.t * (Environ.env * Evd.evar_map) option * Val.t * string
+
+let () = CErrors.register_handler begin function
+| CoercionError (id, env, v, s) ->
+ Some (str "Ltac variable " ++ Id.print id ++
strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
strbrk "which cannot be coerced to " ++ str s ++ str".")
+| _ -> None
+end
+
+let error_ltac_variable ?loc id env v s =
+ Loc.raise ?loc (CoercionError (id, env, v, s))
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index b8592c5c76..8ca2510459 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -69,7 +69,7 @@ val coerce_to_uconstr : Value.t -> Ltac_pretype.closed_glob_constr
val coerce_to_closed_constr : Environ.env -> Value.t -> constr
val coerce_to_evaluable_ref :
- Environ.env -> Evd.evar_map -> Value.t -> evaluable_global_reference
+ Environ.env -> Evd.evar_map -> Value.t -> Tacred.evaluable_global_reference
val coerce_to_constr_list : Environ.env -> Value.t -> constr list
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 7b2c8e1d04..a880a3305e 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -270,7 +270,7 @@ constraint 'a = <
type g_trm = Genintern.glob_constr_and_expr
type g_pat = Genintern.glob_constr_pattern_and_expr
-type g_cst = evaluable_global_reference Genredexpr.and_short_name or_var
+type g_cst = Tacred.evaluable_global_reference Genredexpr.and_short_name or_var
type g_ref = ltac_constant located or_var
type g_nam = lident
@@ -324,7 +324,7 @@ type raw_tactic_arg =
type t_trm = EConstr.constr
type t_pat = constr_pattern
-type t_cst = evaluable_global_reference
+type t_cst = Tacred.evaluable_global_reference
type t_ref = ltac_constant located
type t_nam = Id.t
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 2382dcfbb9..3bb20b9d19 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -269,7 +269,7 @@ constraint 'a = <
type g_trm = Genintern.glob_constr_and_expr
type g_pat = Genintern.glob_constr_pattern_and_expr
-type g_cst = evaluable_global_reference Genredexpr.and_short_name or_var
+type g_cst = Tacred.evaluable_global_reference Genredexpr.and_short_name or_var
type g_ref = ltac_constant located or_var
type g_nam = lident
@@ -323,7 +323,7 @@ type raw_tactic_arg =
type t_trm = EConstr.constr
type t_pat = constr_pattern
-type t_cst = evaluable_global_reference
+type t_cst = Tacred.evaluable_global_reference
type t_ref = ltac_constant located
type t_nam = Id.t
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 8bee7afa2c..ae7a10ce52 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -308,8 +308,8 @@ let short_name qid =
else None
let evalref_of_globref ?loc ?short = function
- | GlobRef.ConstRef cst -> ArgArg (EvalConstRef cst, short)
- | GlobRef.VarRef id -> ArgArg (EvalVarRef id, short)
+ | GlobRef.ConstRef cst -> ArgArg (Tacred.EvalConstRef cst, short)
+ | GlobRef.VarRef id -> ArgArg (Tacred.EvalVarRef id, short)
| r ->
let tpe = match r with
| GlobRef.IndRef _ -> "inductive"
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 90546ea939..6148f0d23f 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -89,7 +89,7 @@ let subst_global_reference subst =
Locusops.or_var_map (subst_located (subst_global_reference subst))
let subst_evaluable subst =
- let subst_eval_ref = subst_evaluable_reference subst in
+ let subst_eval_ref = Tacred.subst_evaluable_reference subst in
Locusops.or_var_map (subst_and_short_name subst_eval_ref)
let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c)
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index a7b571d3db..7d959aa788 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -189,6 +189,7 @@ let flatten_contravariant_disj _ ist =
| _ -> fail
let evalglobref_of_globref =
+ let open Tacred in
function
| GlobRef.VarRef v -> EvalVarRef v
| GlobRef.ConstRef c -> EvalConstRef c
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 05:21:28 +0000