aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/coretactics.mlg2
-rw-r--r--plugins/ltac/extraargs.mlg4
-rw-r--r--plugins/ltac/extratactics.mlg4
-rw-r--r--plugins/ltac/g_auto.mlg2
-rw-r--r--plugins/ltac/g_class.mlg12
-rw-r--r--plugins/ltac/g_obligations.mlg2
-rw-r--r--plugins/ltac/g_rewrite.mlg2
-rw-r--r--plugins/ltac/g_tactic.mlg2
-rw-r--r--plugins/ltac/pptactic.ml2
-rw-r--r--plugins/ltac/rewrite.ml70
-rw-r--r--plugins/ltac/taccoerce.ml28
-rw-r--r--plugins/ltac/tacentries.ml4
-rw-r--r--plugins/ltac/tacintern.ml2
-rw-r--r--plugins/ltac/tacinterp.ml14
-rw-r--r--plugins/ltac/tacsubst.ml2
15 files changed, 59 insertions, 93 deletions
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index f1f538ab39..b7ac71181a 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -20,8 +20,6 @@ open Tacarg
open Names
open Logic
-let wit_hyp = wit_var
-
}
DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index 863c4d37d8..ad4374dba3 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -47,7 +47,7 @@ let () =
let () =
let register name entry = Tacentries.register_tactic_notation_entry name entry in
- register "hyp" wit_var;
+ register "hyp" wit_hyp;
register "simple_intropattern" wit_simple_intropattern;
register "integer" wit_integer;
register "reference" wit_ref;
@@ -140,7 +140,7 @@ ARGUMENT EXTEND occurrences
GLOB_PRINTED BY { pr_occurrences }
| [ ne_integer_list(l) ] -> { ArgArg l }
-| [ var(id) ] -> { ArgVar id }
+| [ hyp(id) ] -> { ArgVar id }
END
{
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 4f20e5a800..a2a47c0bf4 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -33,8 +33,6 @@ open Proofview.Notations
open Attributes
open Vernacextend
-let wit_hyp = wit_var
-
}
DECLARE PLUGIN "ltac_plugin"
@@ -450,7 +448,7 @@ END
(* Subst *)
TACTIC EXTEND subst
-| [ "subst" ne_var_list(l) ] -> { subst l }
+| [ "subst" ne_hyp_list(l) ] -> { subst l }
| [ "subst" ] -> { subst_all () }
END
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 2e72ceae5a..44472a1995 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -18,8 +18,6 @@ open Pcoq.Constr
open Pltac
open Hints
-let wit_hyp = wit_var
-
}
DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 8d197e6056..8c2e633be5 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -31,12 +31,12 @@ let set_transparency cl b =
}
VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF
-| [ "Typeclasses" "Transparent" reference_list(cl) ] -> {
+| [ "Typeclasses" "Transparent" ne_reference_list(cl) ] -> {
set_transparency cl true }
END
VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF
-| [ "Typeclasses" "Opaque" reference_list(cl) ] -> {
+| [ "Typeclasses" "Opaque" ne_reference_list(cl) ] -> {
set_transparency cl false }
END
@@ -77,7 +77,7 @@ END
(* true = All transparent, false = Opaque if possible *)
VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) integer_opt(depth) ] -> {
+ | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) natural_opt(depth) ] -> {
set_typeclasses_debug d;
Option.iter set_typeclasses_strategy s;
set_typeclasses_depth depth
@@ -87,11 +87,13 @@ END
(** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *)
TACTIC EXTEND typeclasses_eauto
| [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
- { typeclasses_eauto ~strategy:Bfs ~depth:d l }
+ { typeclasses_eauto ~depth:d ~strategy:Bfs l }
| [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
{ typeclasses_eauto ~depth:d l }
+ | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) ] -> {
+ typeclasses_eauto ~depth:d ~strategy:Bfs ~only_classes:true [Class_tactics.typeclasses_db] }
| [ "typeclasses" "eauto" int_or_var_opt(d) ] -> {
- typeclasses_eauto ~only_classes:true ~depth:d [Class_tactics.typeclasses_db] }
+ typeclasses_eauto ~depth:d ~only_classes:true [Class_tactics.typeclasses_db] }
END
TACTIC EXTEND head_of_constr
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index fc24475a62..6bf330c830 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -111,6 +111,8 @@ END
VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF STATE program
| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] ->
{ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) }
+| [ "Solve" "Obligations" "of" ident(name) ] ->
+ { try_solve_obligations (Some name) None }
| [ "Solve" "Obligations" "with" tactic(t) ] ->
{ try_solve_obligations None (Some (Tacinterp.interp t)) }
| [ "Solve" "Obligations" ] ->
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 8331927cda..ee94fd565a 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -29,8 +29,6 @@ open Pvernac.Vernac_
open Pltac
open Vernacextend
-let wit_hyp = wit_var
-
}
DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index e51b1f051d..c186a83a5c 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -280,7 +280,7 @@ GRAMMAR EXTEND Gram
| "[="; tc = intropatterns; "]" -> { IntroInjection tc } ] ]
;
naming_intropattern:
- [ [ prefix = pattern_ident -> { IntroFresh prefix }
+ [ [ prefix = pattern_ident -> { IntroFresh prefix.CAst.v }
| "?" -> { IntroAnonymous }
| id = ident -> { IntroIdentifier id } ] ]
;
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index cbb53497d3..fe896f9351 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1323,7 +1323,7 @@ let () =
register_basic_print0 wit_smart_global
(pr_or_by_notation pr_qualid) (pr_or_var (pr_located pr_global)) pr_global;
register_basic_print0 wit_ident pr_id pr_id pr_id;
- register_basic_print0 wit_var pr_lident pr_lident pr_id;
+ register_basic_print0 wit_hyp pr_lident pr_lident pr_id;
register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"];
register_print0 wit_simple_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env;
Genprint.register_print0
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 5ef76dbdc1..9bb435f4dc 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -769,7 +769,7 @@ let get_rew_prf evars r = match r.rew_prf with
let poly_subrelation sort =
if sort then PropGlobal.subrelation else TypeGlobal.subrelation
-let resolve_subrelation env avoid car rel sort prf rel' res =
+let resolve_subrelation env car rel sort prf rel' res =
if Termops.eq_constr (fst res.rew_evars) rel rel' then res
else
let evars, app = app_poly_check env res.rew_evars (poly_subrelation sort) [|car; rel; rel'|] in
@@ -779,7 +779,7 @@ let resolve_subrelation env avoid car rel sort prf rel' res =
rew_prf = RewPrf (rel', appsub);
rew_evars = evars }
-let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) evars =
+let resolve_morphism env m args args' (b,cstr) evars =
let evars, morph_instance, proj, sigargs, m', args, args' =
let first = match (Array.findi (fun _ b -> not (Option.is_empty b)) args') with
| Some i -> i
@@ -843,18 +843,18 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
let proof = applist (proj, List.rev projargs) in
let newt = applist (m', List.rev typeargs) in
match respars with
- [ a, Some r ] -> evars, proof, substl subst a, substl subst r, oldt, fnewt newt
+ [ a, Some r ] -> evars, proof, substl subst a, substl subst r, newt
| _ -> assert(false)
-let apply_constraint env avoid car rel prf cstr res =
+let apply_constraint env car rel prf cstr res =
match snd cstr with
| None -> res
- | Some r -> resolve_subrelation env avoid car rel (fst cstr) prf r res
+ | Some r -> resolve_subrelation env car rel (fst cstr) prf r res
-let coerce env avoid cstr res =
+let coerce env cstr res =
let evars, (rel, prf) = get_rew_prf res.rew_evars res in
let res = { res with rew_evars = evars } in
- apply_constraint env avoid res.rew_car rel prf cstr res
+ 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
@@ -863,7 +863,7 @@ let apply_rule unify loccs : int pure_strategy =
then List.mem occ occs
else not (List.mem occ occs)
in
- { strategy = fun { state = occ ; env ; unfresh ;
+ { strategy = fun { state = occ ; 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
@@ -874,7 +874,7 @@ let apply_rule unify loccs : int pure_strategy =
else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity)
else
let res = { rew with rew_car = ty } in
- let res = Success (coerce env unfresh cstr res) in
+ let res = Success (coerce env cstr res) in
(occ, res)
}
@@ -1017,10 +1017,10 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| None -> false
| Some r -> not (is_rew_cast r.rew_prf)) args'
then
- let evars', prf, car, rel, c1, c2 =
- resolve_morphism env unfresh t m args args' (prop, cstr') evars'
+ let evars', prf, car, rel, c2 =
+ resolve_morphism env m args args' (prop, cstr') evars'
in
- let res = { rew_car = ty; rew_from = c1;
+ let res = { rew_car = ty; rew_from = t;
rew_to = c2; rew_prf = RewPrf (rel, prf);
rew_evars = evars' }
in Success res
@@ -1071,7 +1071,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let res =
match prf with
| RewPrf (rel, prf) ->
- Success (apply_constraint env unfresh res.rew_car
+ Success (apply_constraint env res.rew_car
rel prf (prop,cstr) res)
| _ -> Success res
in state, res
@@ -1094,20 +1094,6 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| Fail | Identity -> res
in state, res
- (* if x' = None && flags.under_lambdas then *)
- (* let lam = mkLambda (n, x, b) in *)
- (* let lam', occ = aux env lam occ None in *)
- (* let res = *)
- (* match lam' with *)
- (* | None -> None *)
- (* | Some (prf, (car, rel, c1, c2)) -> *)
- (* Some (resolve_morphism env sigma t *)
- (* ~fnewt:unfold_all *)
- (* (Lazy.force coq_all) [| x ; lam |] [| None; lam' |] *)
- (* cstr evars) *)
- (* in res, occ *)
- (* else *)
-
| Prod (n, dom, codom) ->
let lam = mkLambda (n, dom, codom) in
let (evars', app), unfold =
@@ -1131,31 +1117,13 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
B. Barras' idea is to have a context of relations, of length 1, with Σ for gluing
dependent relations and using projections to get them out.
*)
- (* | Lambda (n, t, b) when flags.under_lambdas -> *)
- (* let n' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n in *)
- (* let n'' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n' in *)
- (* let n''' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n'' in *)
- (* let rel = new_cstr_evar cstr env (mkApp (Lazy.force coq_relation, [|t|])) in *)
- (* let env' = Environ.push_rel_context [(n'',None,lift 2 rel);(n'',None,lift 1 t);(n', None, t)] env in *)
- (* let b' = s env' avoid b (Typing.type_of env' (goalevars evars) (lift 2 b)) (unlift_cstr env (goalevars evars) cstr) evars in *)
- (* (match b' with *)
- (* | Some (Some r) -> *)
- (* let prf = match r.rew_prf with *)
- (* | RewPrf (rel, prf) -> *)
- (* let rel = pointwise_or_dep_relation n' t r.rew_car rel in *)
- (* let prf = mkLambda (n', t, prf) in *)
- (* RewPrf (rel, prf) *)
- (* | x -> x *)
- (* in *)
- (* Some (Some { r with *)
- (* rew_prf = prf; *)
- (* rew_car = mkProd (n, t, r.rew_car); *)
- (* rew_from = mkLambda(n, t, r.rew_from); *)
- (* rew_to = mkLambda (n, t, r.rew_to) }) *)
- (* | _ -> b') *)
| Lambda (n, t, b) when flags.under_lambdas ->
let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in
+ let unfresh = match n'.binder_name with
+ | Anonymous -> unfresh
+ | Name id -> Id.Set.add id unfresh
+ in
let open Context.Rel.Declaration in
let env' = EConstr.push_rel (LocalAssum (n', t)) env in
let bty = Retyping.get_type_of env' (goalevars evars) b in
@@ -1196,7 +1164,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| Success r ->
let case = mkCase (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 unfresh (prop,cstr) res)
+ state, Success (coerce env (prop,cstr) res)
| Fail | Identity ->
if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then
let evars', eqty = app_poly_sort prop env evars coq_eq [| ty |] in
@@ -1237,7 +1205,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
in
let res =
match res with
- | Success r -> Success (coerce env unfresh (prop,cstr) r)
+ | Success r -> Success (coerce env (prop,cstr) r)
| Fail | Identity -> res
in state, res
| _ -> state, Fail
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index f7037176d2..ee28229cb7 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -161,8 +161,8 @@ let coerce_var_to_ident fresh env sigma v =
match out_gen (topwit wit_intro_pattern) v with
| { CAst.v=IntroNaming (IntroIdentifier id)} -> id
| _ -> fail ()
- else if has_type v (topwit wit_var) then
- out_gen (topwit wit_var) v
+ else if has_type v (topwit wit_hyp) then
+ out_gen (topwit wit_hyp) v
else match Value.to_constr v with
| None -> fail ()
| Some c ->
@@ -184,8 +184,8 @@ let id_of_name = function
| Some (IntroNaming (IntroIdentifier id)) -> id
| Some _ -> fail ()
| None ->
- if has_type v (topwit wit_var) then
- out_gen (topwit wit_var) v
+ if has_type v (topwit wit_hyp) then
+ out_gen (topwit wit_hyp) v
else
match Value.to_constr v with
| None -> fail ()
@@ -222,8 +222,8 @@ let coerce_to_intro_pattern sigma v =
match is_intro_pattern v with
| Some pat -> pat
| None ->
- if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
+ if has_type v (topwit wit_hyp) then
+ let id = out_gen (topwit wit_hyp) v in
IntroNaming (IntroIdentifier id)
else match Value.to_constr v with
| Some c when isVar sigma c ->
@@ -259,8 +259,8 @@ let coerce_to_constr env v =
([], c)
else if has_type v (topwit wit_constr_under_binders) then
out_gen (topwit wit_constr_under_binders) v
- else if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
+ else if has_type v (topwit wit_hyp) then
+ let id = out_gen (topwit wit_hyp) v in
(try [], constr_of_id env id with Not_found -> fail ())
else fail ()
@@ -282,8 +282,8 @@ let coerce_to_evaluable_ref env sigma v =
| Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> EvalVarRef id
| Some _ -> fail ()
| None ->
- if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
+ if has_type v (topwit wit_hyp) then
+ let id = out_gen (topwit wit_hyp) v in
if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id
else fail ()
else if has_type v (topwit wit_ref) then
@@ -328,8 +328,8 @@ let coerce_to_hyp env sigma v =
| Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> id
| Some _ -> fail ()
| None ->
- if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
+ if has_type v (topwit wit_hyp) then
+ let id = out_gen (topwit wit_hyp) v in
if is_variable env id then id else fail ()
else match Value.to_constr v with
| Some c when isVar sigma c -> destVar sigma c
@@ -360,8 +360,8 @@ let coerce_to_quantified_hypothesis sigma v =
| Some (IntroNaming (IntroIdentifier id)) -> NamedHyp id
| Some _ -> raise (CannotCoerceTo "a quantified hypothesis")
| None ->
- if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
+ if has_type v (topwit wit_hyp) then
+ let id = out_gen (topwit wit_hyp) v in
NamedHyp id
else if has_type v (topwit wit_int) then
AnonHyp (out_gen (topwit wit_int) v)
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index f0ca813b08..d58a76fe13 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -219,7 +219,9 @@ let interp_prod_item = function
| None ->
if String.Map.mem s !entry_names then String.Map.find s !entry_names
else begin match ArgT.name s with
- | None -> user_err Pp.(str ("Unknown entry "^s^"."))
+ | None ->
+ if s = "var" then user_err Pp.(str ("var is deprecated, use hyp.")) (* to remove in 8.14 *)
+ else user_err Pp.(str ("Unknown entry "^s^"."))
| Some arg -> arg
end
| Some n ->
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index dea216045e..9c3b05fdf1 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -835,7 +835,7 @@ let () =
Genintern.register_intern0 wit_ref (lift intern_global_reference);
Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c));
Genintern.register_intern0 wit_ident intern_ident';
- Genintern.register_intern0 wit_var (lift intern_hyp);
+ Genintern.register_intern0 wit_hyp (lift intern_hyp);
Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
Genintern.register_intern0 wit_ltac (lift intern_ltac);
Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis);
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index eaeae50254..12bfb4d09e 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -971,8 +971,8 @@ let interp_destruction_arg ist gl arg =
match v with
| {v=IntroNaming (IntroIdentifier id)} -> try_cast_id id
| _ -> error ()
- else if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
+ else if has_type v (topwit wit_hyp) then
+ let id = out_gen (topwit wit_hyp) v in
try_cast_id id
else if has_type v (topwit wit_int) then
keep,ElimOnAnonHyp (out_gen (topwit wit_int) v)
@@ -1238,7 +1238,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
| ArgVar {loc;v=id} ->
let v =
try Id.Map.find id ist.lfun
- with Not_found -> in_gen (topwit wit_var) id
+ with Not_found -> in_gen (topwit wit_hyp) id
in
let open Ftactic in
force_vrec ist v >>= begin fun v ->
@@ -1529,7 +1529,7 @@ and interp_genarg ist x : Val.t Ftactic.t =
let open Ftactic.Notations in
(* Ad-hoc handling of some types. *)
let tag = genarg_tag x in
- if argument_type_eq tag (unquote (topwit (wit_list wit_var))) then
+ if argument_type_eq tag (unquote (topwit (wit_list wit_hyp))) then
interp_genarg_var_list ist x
else if argument_type_eq tag (unquote (topwit (wit_list wit_constr))) then
interp_genarg_constr_list ist x
@@ -1573,9 +1573,9 @@ and interp_genarg_var_list ist x =
Ftactic.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
- let lc = Genarg.out_gen (glbwit (wit_list wit_var)) x in
+ let lc = Genarg.out_gen (glbwit (wit_list wit_hyp)) x in
let lc = interp_hyp_list ist env sigma lc in
- let lc = in_list (val_tag wit_var) lc in
+ let lc = in_list (val_tag wit_hyp) lc in
Ftactic.return lc
end
@@ -2096,7 +2096,7 @@ let () =
register_interp0 wit_ref (lift interp_reference);
register_interp0 wit_pre_ident (lift interp_pre_ident);
register_interp0 wit_ident (lift interp_ident);
- register_interp0 wit_var (lift interp_hyp);
+ register_interp0 wit_hyp (lift interp_hyp);
register_interp0 wit_intropattern (lifts interp_intro_pattern) [@warning "-3"];
register_interp0 wit_simple_intropattern (lifts interp_intro_pattern);
register_interp0 wit_clause_dft_concl (lift interp_clause);
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index fd869b225f..ec44ae4698 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -282,7 +282,7 @@ let () =
Genintern.register_subst0 wit_smart_global subst_global_reference;
Genintern.register_subst0 wit_pre_ident (fun _ v -> v);
Genintern.register_subst0 wit_ident (fun _ v -> v);
- Genintern.register_subst0 wit_var (fun _ v -> v);
+ Genintern.register_subst0 wit_hyp (fun _ v -> v);
Genintern.register_subst0 wit_intropattern subst_intro_pattern [@warning "-3"];
Genintern.register_subst0 wit_simple_intropattern subst_intro_pattern;
Genintern.register_subst0 wit_tactic subst_tactic;
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 06:39:00 +0000