aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/g_ltac2.ml423
-rw-r--r--src/tac2core.ml6
-rw-r--r--src/tac2entries.ml29
-rw-r--r--src/tac2env.ml75
-rw-r--r--src/tac2env.mli17
-rw-r--r--src/tac2expr.mli9
-rw-r--r--src/tac2intern.ml120
-rw-r--r--src/tac2print.ml4
8 files changed, 143 insertions, 140 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 605cb75d66..88a64dacd9 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -28,20 +28,32 @@ let inj_constr loc c = inj_wit Stdarg.wit_constr loc c
let inj_open_constr loc c = inj_wit Stdarg.wit_open_constr loc c
let inj_ident loc c = inj_wit Stdarg.wit_ident loc c
+let pattern_of_qualid loc id =
+ if Tac2env.is_constructor (snd id) then CPatRef (loc, RelId id, [])
+ else
+ let (dp, id) = Libnames.repr_qualid (snd id) in
+ if DirPath.is_empty dp then CPatVar (Some loc, Name id)
+ else
+ CErrors.user_err ~loc (Pp.str "Syntax error")
+
GEXTEND Gram
GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn;
tac2pat:
[ "1" LEFTA
- [ id = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" -> CPatRef (!@loc, RelId id, pl)
- | id = Prim.qualid -> CPatRef (!@loc, RelId id, [])
+ [ id = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" ->
+ if Tac2env.is_constructor (snd id) then
+ CPatRef (!@loc, RelId id, pl)
+ else
+ CErrors.user_err ~loc:!@loc (Pp.str "Syntax error")
+ | id = Prim.qualid -> pattern_of_qualid !@loc id
| "["; "]" -> CPatRef (!@loc, AbsKn Tac2core.Core.c_nil, [])
| p1 = tac2pat; "::"; p2 = tac2pat ->
CPatRef (!@loc, AbsKn Tac2core.Core.c_cons, [p1; p2])
]
| "0"
- [ "_" -> CPatAny (!@loc)
+ [ "_" -> CPatVar (Some !@loc, Anonymous)
| "()" -> CPatTup (Loc.tag ~loc:!@loc [])
- | id = Prim.qualid -> CPatRef (!@loc, RelId id, [])
+ | id = Prim.qualid -> pattern_of_qualid !@loc id
| "("; pl = LIST0 tac2pat LEVEL "1" SEP ","; ")" -> CPatTup (Loc.tag ~loc:!@loc pl) ]
]
;
@@ -90,7 +102,8 @@ GEXTEND Gram
tactic_atom:
[ [ n = Prim.integer -> CTacAtm (Loc.tag ~loc:!@loc (AtmInt n))
| s = Prim.string -> CTacAtm (Loc.tag ~loc:!@loc (AtmStr s))
- | id = Prim.qualid -> CTacRef (RelId id)
+ | id = Prim.qualid ->
+ if Tac2env.is_constructor (snd id) then CTacCst (RelId id) else CTacRef (RelId id)
| "@"; id = Prim.ident -> inj_ident !@loc id
| "'"; c = Constr.constr -> inj_open_constr !@loc c
| IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_constr !@loc c
diff --git a/src/tac2core.ml b/src/tac2core.ml
index b665f761ce..2ccc49b043 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -734,7 +734,7 @@ let dummy_loc = Loc.make_loc (-1, -1)
let rthunk e =
let loc = Tac2intern.loc_of_tacexpr e in
- let var = [CPatAny loc, Some (CTypRef (loc, AbsKn Core.t_unit, []))] in
+ let var = [CPatVar (Some loc, Anonymous), Some (CTypRef (loc, AbsKn Core.t_unit, []))] in
CTacFun (loc, var, e)
let add_generic_scope s entry arg =
@@ -795,9 +795,9 @@ let () = add_scope "opt" begin function
let scope = Extend.Aopt scope in
let act opt = match opt with
| None ->
- CTacRef (AbsKn (TacConstructor Core.c_none))
+ CTacCst (AbsKn Core.c_none)
| Some x ->
- CTacApp (dummy_loc, CTacRef (AbsKn (TacConstructor Core.c_some)), [act x])
+ CTacApp (dummy_loc, CTacCst (AbsKn Core.c_some), [act x])
in
Tac2entries.ScopeRule (scope, act)
| _ -> scope_fail ()
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 100041f15e..da0e213340 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -34,14 +34,14 @@ type tacdef = {
}
let perform_tacdef visibility ((sp, kn), def) =
- let () = if not def.tacdef_local then Tac2env.push_ltac visibility sp (TacConstant kn) in
+ let () = if not def.tacdef_local then Tac2env.push_ltac visibility sp kn in
Tac2env.define_global kn (def.tacdef_expr, def.tacdef_type)
let load_tacdef i obj = perform_tacdef (Until i) obj
let open_tacdef i obj = perform_tacdef (Exactly i) obj
let cache_tacdef ((sp, kn), def) =
- let () = Tac2env.push_ltac (Until 1) sp (TacConstant kn) in
+ let () = Tac2env.push_ltac (Until 1) sp kn in
Tac2env.define_global kn (def.tacdef_expr, def.tacdef_type)
let subst_tacdef (subst, def) =
@@ -83,7 +83,7 @@ let push_typedef visibility sp kn (_, def) = match def with
let iter (c, _) =
let spc = change_sp_label sp c in
let knc = change_kn_label kn c in
- Tac2env.push_ltac visibility spc (TacConstructor knc)
+ Tac2env.push_constructor visibility spc knc
in
Tac2env.push_type visibility sp kn;
List.iter iter cstrs
@@ -185,7 +185,7 @@ let push_typext vis sp kn def =
let iter data =
let spc = change_sp_label sp data.edata_name in
let knc = change_kn_label kn data.edata_name in
- Tac2env.push_ltac vis spc (TacConstructor knc)
+ Tac2env.push_constructor vis spc knc
in
List.iter iter def.typext_expr
@@ -620,12 +620,18 @@ let register_struct ?local str = match str with
let print_ltac ref =
let (loc, qid) = qualid_of_reference ref in
- let kn =
- try Tac2env.locate_ltac qid
- with Not_found -> user_err ?loc (str "Unknown tactic " ++ pr_qualid qid)
- in
- match kn with
- | TacConstant kn ->
+ if Tac2env.is_constructor qid then
+ let kn =
+ try Tac2env.locate_constructor qid
+ with Not_found -> user_err ?loc (str "Unknown constructor " ++ pr_qualid qid)
+ in
+ let _ = Tac2env.interp_constructor kn in
+ Feedback.msg_notice (hov 2 (str "Constructor" ++ spc () ++ str ":" ++ spc () ++ pr_qualid qid))
+ else
+ let kn =
+ try Tac2env.locate_ltac qid
+ with Not_found -> user_err ?loc (str "Unknown tactic " ++ pr_qualid qid)
+ in
let (e, _, (_, t)) = Tac2env.interp_global kn in
let name = int_name () in
Feedback.msg_notice (
@@ -634,9 +640,6 @@ let print_ltac ref =
hov 2 (pr_qualid qid ++ spc () ++ str ":=" ++ spc () ++ pr_glbexpr e)
)
)
- | TacConstructor kn ->
- let _ = Tac2env.interp_constructor kn in
- Feedback.msg_notice (hov 2 (str "Constructor" ++ spc () ++ str ":" ++ spc () ++ pr_qualid qid))
(** Calling tactics *)
diff --git a/src/tac2env.ml b/src/tac2env.ml
index 08c7b321be..6e47e78a9d 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -115,25 +115,13 @@ struct
id, (DirPath.repr dir)
end
-type tacref = Tac2expr.tacref =
-| TacConstant of ltac_constant
-| TacConstructor of ltac_constructor
-
-module TacRef =
-struct
-type t = tacref
-let equal r1 r2 = match r1, r2 with
-| TacConstant c1, TacConstant c2 -> KerName.equal c1 c2
-| TacConstructor c1, TacConstructor c2 -> KerName.equal c1 c2
-| _ -> false
-end
-
module KnTab = Nametab.Make(FullPath)(KerName)
-module RfTab = Nametab.Make(FullPath)(TacRef)
type nametab = {
- tab_ltac : RfTab.t;
- tab_ltac_rev : full_path KNmap.t * full_path KNmap.t;
+ tab_ltac : KnTab.t;
+ tab_ltac_rev : full_path KNmap.t;
+ tab_cstr : KnTab.t;
+ tab_cstr_rev : full_path KNmap.t;
tab_type : KnTab.t;
tab_type_rev : full_path KNmap.t;
tab_proj : KnTab.t;
@@ -141,8 +129,10 @@ type nametab = {
}
let empty_nametab = {
- tab_ltac = RfTab.empty;
- tab_ltac_rev = (KNmap.empty, KNmap.empty);
+ tab_ltac = KnTab.empty;
+ tab_ltac_rev = KNmap.empty;
+ tab_cstr = KnTab.empty;
+ tab_cstr_rev = KNmap.empty;
tab_type = KnTab.empty;
tab_type_rev = KNmap.empty;
tab_proj = KnTab.empty;
@@ -153,29 +143,41 @@ let nametab = Summary.ref empty_nametab ~name:"ltac2-nametab"
let push_ltac vis sp kn =
let tab = !nametab in
- let tab_ltac = RfTab.push vis sp kn tab.tab_ltac in
- let (constant_map, constructor_map) = tab.tab_ltac_rev in
- let tab_ltac_rev = match kn with
- | TacConstant c -> (KNmap.add c sp constant_map, constructor_map)
- | TacConstructor c -> (constant_map, KNmap.add c sp constructor_map)
- in
+ let tab_ltac = KnTab.push vis sp kn tab.tab_ltac in
+ let tab_ltac_rev = KNmap.add kn sp tab.tab_ltac_rev in
nametab := { tab with tab_ltac; tab_ltac_rev }
let locate_ltac qid =
let tab = !nametab in
- RfTab.locate qid tab.tab_ltac
+ KnTab.locate qid tab.tab_ltac
let locate_extended_all_ltac qid =
let tab = !nametab in
- RfTab.find_prefixes qid tab.tab_ltac
+ KnTab.find_prefixes qid tab.tab_ltac
let shortest_qualid_of_ltac kn =
let tab = !nametab in
- let sp = match kn with
- | TacConstant c -> KNmap.find c (fst tab.tab_ltac_rev)
- | TacConstructor c -> KNmap.find c (snd tab.tab_ltac_rev)
- in
- RfTab.shortest_qualid Id.Set.empty sp tab.tab_ltac
+ let sp = KNmap.find kn tab.tab_ltac_rev in
+ KnTab.shortest_qualid Id.Set.empty sp tab.tab_ltac
+
+let push_constructor vis sp kn =
+ let tab = !nametab in
+ let tab_cstr = KnTab.push vis sp kn tab.tab_cstr in
+ let tab_cstr_rev = KNmap.add kn sp tab.tab_cstr_rev in
+ nametab := { tab with tab_cstr; tab_cstr_rev }
+
+let locate_constructor qid =
+ let tab = !nametab in
+ KnTab.locate qid tab.tab_cstr
+
+let locate_extended_all_constructor qid =
+ let tab = !nametab in
+ KnTab.find_prefixes qid tab.tab_cstr
+
+let shortest_qualid_of_constructor kn =
+ let tab = !nametab in
+ let sp = KNmap.find kn tab.tab_cstr_rev in
+ KnTab.shortest_qualid Id.Set.empty sp tab.tab_cstr
let push_type vis sp kn =
let tab = !nametab in
@@ -240,3 +242,14 @@ let coq_prefix =
(** Generic arguments *)
let wit_ltac2 = Genarg.make0 "ltac2"
+
+let is_constructor qid =
+ let (_, id) = repr_qualid qid in
+ let id = Id.to_string id in
+ assert (String.length id > 0);
+ match id with
+ | "true" | "false" -> true (** built-in constructors *)
+ | _ ->
+ match id.[0] with
+ | 'A'..'Z' -> true
+ | _ -> false
diff --git a/src/tac2env.mli b/src/tac2env.mli
index c4b8c1e0ca..8ab9656cb9 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -63,10 +63,15 @@ val interp_projection : ltac_projection -> projection_data
(** {5 Name management} *)
-val push_ltac : visibility -> full_path -> tacref -> unit
-val locate_ltac : qualid -> tacref
-val locate_extended_all_ltac : qualid -> tacref list
-val shortest_qualid_of_ltac : tacref -> qualid
+val push_ltac : visibility -> full_path -> ltac_constant -> unit
+val locate_ltac : qualid -> ltac_constant
+val locate_extended_all_ltac : qualid -> ltac_constant list
+val shortest_qualid_of_ltac : ltac_constant -> qualid
+
+val push_constructor : visibility -> full_path -> ltac_constructor -> unit
+val locate_constructor : qualid -> ltac_constructor
+val locate_extended_all_constructor : qualid -> ltac_constructor list
+val shortest_qualid_of_constructor : ltac_constructor -> qualid
val push_type : visibility -> full_path -> type_constant -> unit
val locate_type : qualid -> type_constant
@@ -104,3 +109,7 @@ val coq_prefix : ModPath.t
(** {5 Generic arguments} *)
val wit_ltac2 : (raw_tacexpr, glb_tacexpr, Util.Empty.t) genarg_type
+
+(** {5 Helper functions} *)
+
+val is_constructor : qualid -> bool
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index a9f2109cb2..b268e70cb3 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -70,19 +70,16 @@ type atom =
| AtmInt of int
| AtmStr of string
-type tacref =
-| TacConstant of ltac_constant
-| TacConstructor of ltac_constructor
-
(** Tactic expressions *)
type raw_patexpr =
-| CPatAny of Loc.t
+| CPatVar of Name.t located
| CPatRef of Loc.t * ltac_constructor or_relid * raw_patexpr list
| CPatTup of raw_patexpr list located
type raw_tacexpr =
| CTacAtm of atom located
-| CTacRef of tacref or_relid
+| CTacRef of ltac_constant or_relid
+| CTacCst of ltac_constructor or_relid
| CTacFun of Loc.t * (raw_patexpr * raw_typexpr option) list * raw_tacexpr
| CTacApp of Loc.t * raw_tacexpr * raw_tacexpr list
| CTacLet of Loc.t * rec_flag * (Name.t located * raw_typexpr option * raw_tacexpr) list * raw_tacexpr
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index 79e33f3a94..3ea35171bb 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -191,6 +191,8 @@ let loc_of_tacexpr = function
| CTacAtm (loc, _) -> Option.default dummy_loc loc
| CTacRef (RelId (loc, _)) -> Option.default dummy_loc loc
| CTacRef (AbsKn _) -> dummy_loc
+| CTacCst (RelId (loc, _)) -> Option.default dummy_loc loc
+| CTacCst (AbsKn _) -> dummy_loc
| CTacFun (loc, _, _) -> loc
| CTacApp (loc, _, _) -> loc
| CTacLet (loc, _, _, _) -> loc
@@ -206,7 +208,7 @@ let loc_of_tacexpr = function
| CTacExt (loc, _) -> loc
let loc_of_patexpr = function
-| CPatAny loc -> loc
+| CPatVar (loc, _) -> Option.default dummy_loc loc
| CPatRef (loc, _, _) -> loc
| CPatTup (loc, _) -> Option.default dummy_loc loc
@@ -516,22 +518,17 @@ let get_variable env var =
let get_constructor env var = match var with
| RelId (loc, qid) ->
- let c = try Some (Tac2env.locate_ltac qid) with Not_found -> None in
+ let c = try Some (Tac2env.locate_constructor qid) with Not_found -> None in
begin match c with
- | Some (TacConstructor knc) ->
+ | Some knc ->
let kn = Tac2env.interp_constructor knc in
- ArgArg (kn, knc)
- | Some (TacConstant _) ->
- CErrors.user_err ?loc (str "The term " ++ pr_qualid qid ++
- str " is not the constructor of an inductive type.")
+ (kn, knc)
| None ->
- let (dp, id) = repr_qualid qid in
- if DirPath.is_empty dp then ArgVar (loc, id)
- else CErrors.user_err ?loc (str "Unbound constructor " ++ pr_qualid qid)
+ CErrors.user_err ?loc (str "Unbound constructor " ++ pr_qualid qid)
end
| AbsKn knc ->
let kn = Tac2env.interp_constructor knc in
- ArgArg (kn, knc)
+ (kn, knc)
let get_projection var = match var with
| RelId (loc, qid) ->
@@ -562,18 +559,10 @@ type glb_patexpr =
| GPatTup of glb_patexpr list
let rec intern_patexpr env = function
-| CPatAny _ -> GPatVar Anonymous
-| CPatRef (_, qid, []) ->
- begin match get_constructor env qid with
- | ArgVar (_, id) -> GPatVar (Name id)
- | ArgArg (_, kn) -> GPatRef (kn, [])
- end
+| CPatVar (_, na) -> GPatVar na
| CPatRef (_, qid, pl) ->
- begin match get_constructor env qid with
- | ArgVar (loc, id) ->
- user_err ?loc (str "Unbound constructor " ++ Nameops.pr_id id)
- | ArgArg (_, kn) -> GPatRef (kn, List.map (fun p -> intern_patexpr env p) pl)
- end
+ let (_, kn) = get_constructor env qid in
+ GPatRef (kn, List.map (fun p -> intern_patexpr env p) pl)
| CPatTup (_, pl) ->
GPatTup (List.map (fun p -> intern_patexpr env p) pl)
@@ -603,10 +592,6 @@ let get_pattern_kind env pl = match pl with
(** Internalization *)
-let is_constructor env qid = match get_variable env qid with
-| ArgArg (TacConstructor _) -> true
-| _ -> false
-
(** Used to generate a fresh tactic variable for pattern-expansion *)
let fresh_var env =
let bad id =
@@ -617,18 +602,19 @@ let fresh_var env =
let rec intern_rec env = function
| CTacAtm (_, atm) -> intern_atm env atm
-| CTacRef qid as e ->
+| CTacRef qid ->
begin match get_variable env qid with
| ArgVar (_, id) ->
let sch = Id.Map.find id env.env_var in
(GTacVar id, fresh_mix_type_scheme env sch)
- | ArgArg (TacConstant kn) ->
+ | ArgArg kn ->
let (_, _, sch) = Tac2env.interp_global kn in
(GTacRef kn, fresh_type_scheme env sch)
- | ArgArg (TacConstructor kn) ->
- let loc = loc_of_tacexpr e in
- intern_constructor env loc kn []
end
+| CTacCst qid as e ->
+ let loc = loc_of_tacexpr e in
+ let (_, kn) = get_constructor env qid in
+ intern_constructor env loc kn []
| CTacFun (loc, bnd, e) ->
let fold (env, bnd, tl) (pat, t) =
let t = match t with
@@ -651,11 +637,8 @@ let rec intern_rec env = function
let (e, t) = intern_rec env e in
let t = List.fold_left (fun accu t -> GTypArrow (t, accu)) t tl in
(GTacFun (bnd, e), t)
-| CTacApp (loc, CTacRef qid, args) as e when is_constructor env qid ->
- let kn = match get_variable env qid with
- | ArgArg (TacConstructor kn) -> kn
- | _ -> assert false
- in
+| CTacApp (loc, CTacCst qid, args) as e ->
+ let (_, kn) = get_constructor env qid in
let loc = loc_of_tacexpr e in
intern_constructor env loc kn args
| CTacApp (loc, f, args) ->
@@ -823,7 +806,7 @@ and intern_let_rec env loc el e =
to depth-one where leaves are either variables or catch-all *)
and intern_case env loc e pl =
let (e', t) = intern_rec env e in
- let todo ~loc () = user_err ~loc (str "Pattern not handled yet") in
+ let todo ?loc () = user_err ?loc (str "Pattern not handled yet") in
match get_pattern_kind env pl with
| PKind_any ->
let (pat, b) = List.hd pl in
@@ -848,12 +831,7 @@ and intern_case env loc e pl =
(GTacCse (e', GCaseAlg t_unit, [|b|], [||]), tb)
| [CPatTup (_, pl), b] ->
let map = function
- | CPatAny _ -> Anonymous
- | CPatRef (loc, qid, []) ->
- begin match get_constructor env qid with
- | ArgVar (_, id) -> Name id
- | ArgArg _ -> todo ~loc ()
- end
+ | CPatVar (_, na) -> na
| p -> todo ~loc:(loc_of_patexpr p) ()
in
let ids = List.map map pl in
@@ -885,7 +863,8 @@ and intern_case env loc e pl =
| [] -> ()
| (pat, br) :: rem ->
let tbr = match pat with
- | CPatAny _ ->
+ | CPatVar (loc, Name _) -> todo ?loc ()
+ | CPatVar (_, Anonymous) ->
let () = check_redundant_clause rem in
let (br', brT) = intern_rec env br in
(** Fill all remaining branches *)
@@ -906,23 +885,14 @@ and intern_case env loc e pl =
let _ = List.fold_left fill (0, 0) cstrs in
brT
| CPatRef (loc, qid, args) ->
- let data = match get_constructor env qid with
- | ArgVar _ -> todo ~loc ()
- | ArgArg (data, _) ->
- let () =
- let kn' = data.cdata_type in
- if not (KerName.equal kn kn') then
- invalid_pattern ~loc kn (GCaseAlg kn')
- in
- data
+ let (data, _) = get_constructor env qid in
+ let () =
+ let kn' = data.cdata_type in
+ if not (KerName.equal kn kn') then
+ invalid_pattern ~loc kn (GCaseAlg kn')
in
let get_id = function
- | CPatAny _ -> Anonymous
- | CPatRef (loc, qid, []) ->
- begin match get_constructor env qid with
- | ArgVar (_, id) -> Name id
- | ArgArg _ -> todo ~loc ()
- end
+ | CPatVar (_, na) -> na
| p -> todo ~loc:(loc_of_patexpr p) ()
in
let ids = List.map get_id args in
@@ -1165,12 +1135,9 @@ let get_projection0 var = match var with
| AbsKn kn -> kn
let rec ids_of_pattern accu = function
-| CPatAny _ -> accu
-| CPatRef (_, RelId (_, qid), pl) ->
- let (dp, id) = repr_qualid qid in
- let accu = if DirPath.is_empty dp then Id.Set.add id accu else accu in
- List.fold_left ids_of_pattern accu pl
-| CPatRef (_, AbsKn _, pl) ->
+| CPatVar (_, Anonymous) -> accu
+| CPatVar (_, Name id) -> Id.Set.add id accu
+| CPatRef (_, _, pl) ->
List.fold_left ids_of_pattern accu pl
| CPatTup (_, pl) ->
List.fold_left ids_of_pattern accu pl
@@ -1183,6 +1150,9 @@ let rec globalize ids e = match e with
| ArgVar _ -> e
| ArgArg kn -> CTacRef (AbsKn kn)
end
+| CTacCst qid ->
+ let (_, knc) = get_constructor () qid in
+ CTacCst (AbsKn knc)
| CTacFun (loc, bnd, e) ->
let fold (pats, accu) (pat, t) =
let accu = ids_of_pattern accu pat in
@@ -1252,12 +1222,10 @@ and globalize_case ids (p, e) =
(globalize_pattern ids p, globalize ids e)
and globalize_pattern ids p = match p with
-| CPatAny _ -> p
+| CPatVar _ -> p
| CPatRef (loc, cst, pl) ->
- let cst = match get_constructor () cst with
- | ArgVar _ -> cst
- | ArgArg (_, knc) -> AbsKn knc
- in
+ let (_, knc) = get_constructor () cst in
+ let cst = AbsKn knc in
let pl = List.map (fun p -> globalize_pattern ids p) pl in
CPatRef (loc, cst, pl)
| CPatTup (loc, pl) ->
@@ -1393,12 +1361,9 @@ let rec subst_rawtype subst t = match t with
let subst_tacref subst ref = match ref with
| RelId _ -> ref
-| AbsKn (TacConstant kn) ->
- let kn' = subst_kn subst kn in
- if kn' == kn then ref else AbsKn (TacConstant kn')
-| AbsKn (TacConstructor kn) ->
+| AbsKn kn ->
let kn' = subst_kn subst kn in
- if kn' == kn then ref else AbsKn (TacConstructor kn')
+ if kn' == kn then ref else AbsKn kn'
let subst_projection subst prj = match prj with
| RelId _ -> prj
@@ -1407,7 +1372,7 @@ let subst_projection subst prj = match prj with
if kn' == kn then prj else AbsKn kn'
let rec subst_rawpattern subst p = match p with
-| CPatAny _ -> p
+| CPatVar _ -> p
| CPatRef (loc, c, pl) ->
let pl' = List.smartmap (fun p -> subst_rawpattern subst p) pl in
let c' = match c with
@@ -1427,6 +1392,9 @@ let rec subst_rawexpr subst t = match t with
| CTacRef ref ->
let ref' = subst_tacref subst ref in
if ref' == ref then t else CTacRef ref'
+| CTacCst ref ->
+ let ref' = subst_tacref subst ref in
+ if ref' == ref then t else CTacCst ref'
| CTacFun (loc, bnd, e) ->
let map (na, t as p) =
let t' = Option.smartmap (fun t -> subst_rawtype subst t) t in
diff --git a/src/tac2print.ml b/src/tac2print.ml
index e6f0582e3d..2afcfb4a6e 100644
--- a/src/tac2print.ml
+++ b/src/tac2print.ml
@@ -83,7 +83,7 @@ let int_name () =
(** Term printing *)
let pr_constructor kn =
- Libnames.pr_qualid (Tac2env.shortest_qualid_of_ltac (TacConstructor kn))
+ Libnames.pr_qualid (Tac2env.shortest_qualid_of_constructor kn)
let pr_projection kn =
Libnames.pr_qualid (Tac2env.shortest_qualid_of_projection kn)
@@ -138,7 +138,7 @@ let pr_glbexpr_gen lvl c =
| GTacAtm atm -> pr_atom atm
| GTacVar id -> Id.print id
| GTacRef gr ->
- let qid = shortest_qualid_of_ltac (TacConstant gr) in
+ let qid = shortest_qualid_of_ltac gr in
Libnames.pr_qualid qid
| GTacFun (nas, c) ->
let nas = pr_sequence pr_name nas in
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 22:57:43 +0000