aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml11
-rw-r--r--interp/constrintern.ml21
-rw-r--r--interp/notation.ml134
-rw-r--r--interp/notation.mli13
-rw-r--r--interp/smartlocate.ml8
-rw-r--r--interp/stdarg.ml2
-rw-r--r--interp/stdarg.mli2
-rw-r--r--interp/syntax_def.ml16
-rw-r--r--interp/syntax_def.mli8
9 files changed, 118 insertions, 97 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index a37bac3275..d5a5bde616 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -435,13 +435,10 @@ let extern_record_pattern cstrsp args =
let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
try
if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
- let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
+ let (na,p,key) = uninterp_prim_token_cases_pattern pat scopes in
match availability_of_entry_coercion custom InConstrEntrySomeLevel with
| None -> raise No_match
| Some coercion ->
- match availability_of_prim_token p sc scopes with
- | None -> raise No_match
- | Some key ->
let loc = cases_pattern_loc pat in
insert_pat_coercion ?loc coercion
(insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na)
@@ -848,13 +845,11 @@ let same_binder_type ty nal c =
(* one with no delimiter if possible) *)
let extern_possible_prim_token (custom,scopes) r =
- let (sc,n) = uninterp_prim_token r in
+ let (n,key) = uninterp_prim_token r scopes in
match availability_of_entry_coercion custom InConstrEntrySomeLevel with
| None -> raise No_match
| Some coercion ->
- match availability_of_prim_token n sc scopes with
- | None -> raise No_match
- | Some key -> insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
+ insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
let filter_enough_applied nargs l =
match nargs with
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f82783f47d..5ad8af6d57 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -187,7 +187,7 @@ let empty_internalization_env = Id.Map.empty
let compute_internalization_data env sigma id ty typ impl =
let impl = compute_implicits_with_manual env sigma typ (is_implicit_args()) impl in
- (ty, impl, compute_arguments_scope sigma typ, var_uid id)
+ (ty, impl, compute_arguments_scope env sigma typ, var_uid id)
let compute_internalization_env env sigma ?(impls=empty_internalization_env) ty =
List.fold_left3
@@ -976,10 +976,6 @@ let split_by_type_pat ?loc ids subst =
assert (terms = [] && termlists = []);
subst
-let make_subst ids l =
- let fold accu (id, scopes) a = Id.Map.add id (a, scopes) accu in
- List.fold_left2 fold Id.Map.empty ids l
-
let intern_notation intern env ntnvars loc ntn fullargs =
(* Adjust to parsing of { } *)
let ntn,fullargs = contract_curly_brackets ntn fullargs in
@@ -1113,8 +1109,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
if List.length args < nids then error_not_enough_arguments ?loc;
let args1,args2 = List.chop nids args in
check_no_explicitation args1;
- let terms = make_subst ids (List.map fst args1) in
- let subst = (terms, Id.Map.empty, Id.Map.empty, Id.Map.empty) in
+ let subst = split_by_type ids (List.map fst args1,[],[],[]) in
let infos = (Id.Map.empty, env) in
let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in
let loc = c.loc in
@@ -1624,8 +1619,8 @@ let drop_notations_pattern looked_for genv =
let nvars = List.length vars in
if List.length pats < nvars then error_not_enough_arguments ?loc:qid.loc;
let pats1,pats2 = List.chop nvars pats in
- let subst = make_subst vars pats1 in
- let idspl1 = List.map (in_not false qid.loc scopes (subst, Id.Map.empty) []) args in
+ let subst = split_by_type_pat vars (pats1,[]) in
+ let idspl1 = List.map (in_not false qid.loc scopes subst []) args in
let (_,argscs) = find_remaining_scopes pats1 pats2 g in
Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2)
| _ -> raise Not_found
@@ -2358,9 +2353,9 @@ let extract_ids env =
(Termops.ids_of_rel_context (Environ.rel_context env))
Id.Set.empty
-let scope_of_type_kind sigma = function
+let scope_of_type_kind env sigma = function
| IsType -> Notation.current_type_scope_name ()
- | OfType typ -> compute_type_scope sigma typ
+ | OfType typ -> compute_type_scope env sigma typ
| WithoutTypeConstraint | UnknownIfTermOrType -> None
let allowed_binder_kind_of_type_kind = function
@@ -2377,7 +2372,7 @@ let empty_ltac_sign = {
let intern_gen kind env sigma
?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
c =
- let tmp_scope = scope_of_type_kind sigma kind in
+ let tmp_scope = scope_of_type_kind env sigma kind in
let k = allowed_binder_kind_of_type_kind kind in
internalize env {ids = extract_ids env; unb = false;
tmp_scope = tmp_scope; scopes = [];
@@ -2462,7 +2457,7 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign)
let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
{ Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c =
- let tmp_scope = scope_of_type_kind sigma kind in
+ let tmp_scope = scope_of_type_kind env sigma kind in
let impls = empty_internalization_env in
let k = allowed_binder_kind_of_type_kind kind in
internalize env
diff --git a/interp/notation.ml b/interp/notation.ml
index 0afbb9cd62..fb3cefd624 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -932,7 +932,7 @@ let prim_token_interp_infos =
(* Table from global_reference to backtrack-able informations about
prim_token uninterpretation (in particular uninterpreter unique id). *)
let prim_token_uninterp_infos =
- ref (GlobRef.Map.empty : (scope_name * prim_token_interp_info * bool) GlobRef.Map.t)
+ ref (GlobRef.Map.empty : ((scope_name * (prim_token_interp_info * bool)) list) GlobRef.Map.t)
let hashtbl_check_and_set allow_overwrite uid f h eq =
match Hashtbl.find h uid with
@@ -968,10 +968,13 @@ let cache_prim_token_interpretation (_,infos) =
check_scope ~tolerant:true sc;
prim_token_interp_infos :=
String.Map.add sc (infos.pt_required,ptii) !prim_token_interp_infos;
- List.iter (fun r -> prim_token_uninterp_infos :=
- GlobRef.Map.add r (sc,ptii,infos.pt_in_match)
- !prim_token_uninterp_infos)
- infos.pt_refs
+ let add_uninterp r =
+ let l = try GlobRef.Map.find r !prim_token_uninterp_infos with Not_found -> [] in
+ let l = List.remove_assoc_f String.equal sc l in
+ prim_token_uninterp_infos :=
+ GlobRef.Map.add r ((sc,(ptii,infos.pt_in_match)) :: l)
+ !prim_token_uninterp_infos in
+ List.iter add_uninterp infos.pt_refs
let subst_prim_token_interpretation (subs,infos) =
{ infos with
@@ -1324,27 +1327,6 @@ let entry_has_ident = function
| InCustomEntryLevel (s,n) ->
try String.Map.find s !entry_has_ident_map <= n with Not_found -> false
-let uninterp_prim_token c =
- match glob_prim_constr_key c with
- | None -> raise Notation_ops.No_match
- | Some r ->
- try
- let (sc,info,_) = GlobRef.Map.find r !prim_token_uninterp_infos in
- let uninterp = match info with
- | Uid uid -> Hashtbl.find prim_token_uninterpreters uid
- | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o)
- | StringNotation o -> InnerPrimToken.StringUninterp (Strings.uninterp o)
- in
- match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with
- | None -> raise Notation_ops.No_match
- | Some n -> (sc,n)
- with Not_found -> raise Notation_ops.No_match
-
-let uninterp_prim_token_cases_pattern c =
- match glob_constr_of_closed_cases_pattern (Global.env()) c with
- | exception Not_found -> raise Notation_ops.No_match
- | na,c -> let (sc,n) = uninterp_prim_token c in (na,sc,n)
-
let availability_of_prim_token n printer_scope local_scopes =
let f scope =
try
@@ -1366,6 +1348,60 @@ let availability_of_prim_token n printer_scope local_scopes =
let scopes = make_current_scopes local_scopes in
Option.map snd (find_without_delimiters f (NotationInScope printer_scope,None) scopes)
+let rec find_uninterpretation need_delim def find = function
+ | [] ->
+ List.find_map
+ (fun (sc,_,_) -> try Some (find need_delim sc) with Not_found -> None)
+ def
+ | OpenScopeItem scope :: scopes ->
+ (try find need_delim scope
+ with Not_found -> find_uninterpretation need_delim def find scopes) (* TODO: here we should also update the need_delim list with all regular notations in scope [scope] that could shadow a numeral notation *)
+ | LonelyNotationItem ntn::scopes ->
+ find_uninterpretation (ntn::need_delim) def find scopes
+
+let uninterp_prim_token c local_scopes =
+ match glob_prim_constr_key c with
+ | None -> raise Notation_ops.No_match
+ | Some r ->
+ let uninterp (sc,(info,_)) =
+ try
+ let uninterp = match info with
+ | Uid uid -> Hashtbl.find prim_token_uninterpreters uid
+ | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o)
+ | StringNotation o -> InnerPrimToken.StringUninterp (Strings.uninterp o)
+ in
+ match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with
+ | None -> None
+ | Some n -> Some (sc,n)
+ with Not_found -> None in
+ let add_key (sc,n) =
+ Option.map (fun k -> sc,n,k) (availability_of_prim_token n sc local_scopes) in
+ let l =
+ try GlobRef.Map.find r !prim_token_uninterp_infos
+ with Not_found -> raise Notation_ops.No_match in
+ let l = List.map_filter uninterp l in
+ let l = List.map_filter add_key l in
+ let find need_delim sc =
+ let _,n,k = List.find (fun (sc',_,_) -> String.equal sc' sc) l in
+ if k <> None then n,k else
+ let hidden =
+ List.exists
+ (fun n' -> notation_eq n' (notation_of_prim_token n))
+ need_delim in
+ if not hidden then n,k else
+ match (String.Map.find sc !scope_map).delimiters with
+ | Some k -> n,Some k
+ | None -> raise Not_found
+ in
+ let scopes = make_current_scopes local_scopes in
+ try find_uninterpretation [] l find scopes
+ with Not_found -> match l with (_,n,k)::_ -> n,k | [] -> raise Notation_ops.No_match
+
+let uninterp_prim_token_cases_pattern c local_scopes =
+ match glob_constr_of_closed_cases_pattern (Global.env()) c with
+ | exception Not_found -> raise Notation_ops.No_match
+ | na,c -> let (sc,n) = uninterp_prim_token c local_scopes in (na,sc,n)
+
(* Miscellaneous *)
let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
@@ -1412,8 +1448,8 @@ type scope_class = cl_typ
let scope_class_compare : scope_class -> scope_class -> int =
cl_typ_ord
-let compute_scope_class sigma t =
- let (cl,_,_) = find_class_type sigma t in
+let compute_scope_class env sigma t =
+ let (cl,_,_) = find_class_type env sigma t in
cl
module ScopeClassOrd =
@@ -1442,22 +1478,23 @@ let find_scope_class_opt = function
(**********************************************************************)
(* Special scopes associated to arguments of a global reference *)
-let rec compute_arguments_classes sigma t =
- match EConstr.kind sigma (Reductionops.whd_betaiotazeta sigma t) with
- | Prod (_,t,u) ->
- let cl = try Some (compute_scope_class sigma t) with Not_found -> None in
- cl :: compute_arguments_classes sigma u
+let rec compute_arguments_classes env sigma t =
+ match EConstr.kind sigma (Reductionops.whd_betaiotazeta env sigma t) with
+ | Prod (na, t, u) ->
+ let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum (na, t)) env in
+ let cl = try Some (compute_scope_class env sigma t) with Not_found -> None in
+ cl :: compute_arguments_classes env sigma u
| _ -> []
-let compute_arguments_scope_full sigma t =
- let cls = compute_arguments_classes sigma t in
+let compute_arguments_scope_full env sigma t =
+ let cls = compute_arguments_classes env sigma t in
let scs = List.map find_scope_class_opt cls in
scs, cls
-let compute_arguments_scope sigma t = fst (compute_arguments_scope_full sigma t)
+let compute_arguments_scope env sigma t = fst (compute_arguments_scope_full env sigma t)
-let compute_type_scope sigma t =
- find_scope_class_opt (try Some (compute_scope_class sigma t) with Not_found -> None)
+let compute_type_scope env sigma t =
+ find_scope_class_opt (try Some (compute_scope_class env sigma t) with Not_found -> None)
let current_type_scope_name () =
find_scope_class_opt (Some CL_SORT)
@@ -1495,15 +1532,16 @@ let load_arguments_scope _ (_,(_,r,n,scl,cls)) =
let cache_arguments_scope o =
load_arguments_scope 1 o
-let subst_scope_class subst cs =
- try Some (subst_cl_typ subst cs) with Not_found -> None
+let subst_scope_class env subst cs =
+ try Some (subst_cl_typ env subst cs) with Not_found -> None
let subst_arguments_scope (subst,(req,r,n,scl,cls)) =
let r' = fst (subst_global subst r) in
let subst_cl ocl = match ocl with
| None -> ocl
| Some cl ->
- match subst_scope_class subst cl with
+ let env = Global.env () in
+ match subst_scope_class env subst cl with
| Some cl' as ocl' when cl' != cl -> ocl'
| _ -> ocl in
let cls' = List.Smart.map subst_cl cls in
@@ -1529,7 +1567,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
| ArgsScopeAuto ->
let env = Global.env () in (*FIXME?*)
let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in
- let scs,cls = compute_arguments_scope_full sigma typ in
+ let scs,cls = compute_arguments_scope_full env sigma typ in
(req,r,List.length scs,scs,cls)
| ArgsScopeManual ->
(* Add to the manually given scopes the one found automatically
@@ -1537,7 +1575,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
of the manually given scopes to avoid further re-computations. *)
let env = Global.env () in (*FIXME?*)
let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in
- let l',cls = compute_arguments_scope_full sigma typ in
+ let l',cls = compute_arguments_scope_full env sigma typ in
let l1 = List.firstn n l' in
let cls1 = List.firstn n cls in
(req,r,0,l1@l,cls1)
@@ -1584,7 +1622,7 @@ let find_arguments_scope r =
let declare_ref_arguments_scope sigma ref =
let env = Global.env () in (* FIXME? *)
let typ = EConstr.of_constr @@ fst @@ Typeops.type_of_global_in_context env ref in
- let (scs,cls as o) = compute_arguments_scope_full sigma typ in
+ let (scs,cls as o) = compute_arguments_scope_full env sigma typ in
declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o
(********************************)
@@ -1771,10 +1809,10 @@ let browse_notation strict ntn map =
map [] in
List.sort (fun x y -> String.compare (snd (fst x)) (snd (fst y))) l
-let global_reference_of_notation test (ntn,(sc,c,_)) =
+let global_reference_of_notation ~head test (ntn,(sc,c,_)) =
match c with
| NRef ref when test ref -> Some (ntn,sc,ref)
- | NApp (NRef ref, l) when List.for_all isNVar_or_NHole l && test ref ->
+ | NApp (NRef ref, l) when head || List.for_all isNVar_or_NHole l && test ref ->
Some (ntn,sc,ref)
| _ -> None
@@ -1786,14 +1824,14 @@ let error_notation_not_reference ?loc ntn =
(str "Unable to interpret " ++ quote (str ntn) ++
str " as a reference.")
-let interp_notation_as_global_reference ?loc test ntn sc =
+let interp_notation_as_global_reference ?loc ~head test ntn sc =
let scopes = match sc with
| Some sc ->
let scope = find_scope (find_delimiters_scope sc) in
String.Map.add sc scope String.Map.empty
| None -> !scope_map in
let ntns = browse_notation true ntn scopes in
- let refs = List.map (global_reference_of_notation test) ntns in
+ let refs = List.map (global_reference_of_notation ~head test) ntns in
match Option.List.flatten refs with
| [_,_,ref] -> ref
| [] -> error_notation_not_reference ?loc ntn
diff --git a/interp/notation.mli b/interp/notation.mli
index 892eba8d11..96a76c4de6 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -206,9 +206,9 @@ val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (GlobRef.t -> unit) ->
raise [No_match] if no such token *)
val uninterp_prim_token :
- 'a glob_constr_g -> scope_name * prim_token
+ 'a glob_constr_g -> subscopes -> prim_token * delimiters option
val uninterp_prim_token_cases_pattern :
- 'a cases_pattern_g -> Name.t * scope_name * prim_token
+ 'a cases_pattern_g -> subscopes -> Name.t * prim_token * delimiters option
val availability_of_prim_token :
prim_token -> scope_name -> subscopes -> delimiters option option
@@ -245,7 +245,8 @@ val availability_of_notation : specific_notation -> subscopes ->
(** {6 Miscellaneous} *)
-val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) ->
+(** If head is true, also allows applied global references. *)
+val interp_notation_as_global_reference : ?loc:Loc.t -> head:bool -> (GlobRef.t -> bool) ->
notation_key -> delimiters option -> GlobRef.t
(** Checks for already existing notations *)
@@ -264,13 +265,13 @@ type scope_class
val scope_class_compare : scope_class -> scope_class -> int
val subst_scope_class :
- Mod_subst.substitution -> scope_class -> scope_class option
+ Environ.env -> Mod_subst.substitution -> scope_class -> scope_class option
val declare_scope_class : scope_name -> scope_class -> unit
val declare_ref_arguments_scope : Evd.evar_map -> GlobRef.t -> unit
-val compute_arguments_scope : Evd.evar_map -> EConstr.types -> scope_name option list
-val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option
+val compute_arguments_scope : Environ.env -> Evd.evar_map -> EConstr.types -> scope_name option list
+val compute_type_scope : Environ.env -> Evd.evar_map -> EConstr.types -> scope_name option
(** Get the current scope bound to Sortclass, if it exists *)
val current_type_scope_name : unit -> scope_name option
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 98fa71e15d..03977fcb4e 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -62,15 +62,15 @@ let global_with_alias ?head qid =
try locate_global_with_alias ?head qid
with Not_found -> Nametab.error_global_not_found qid
-let smart_global ?head = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
+let smart_global ?(head = false) = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
| AN r ->
- global_with_alias ?head r
+ global_with_alias ~head r
| ByNotation (ntn,sc) ->
- Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)
+ Notation.interp_notation_as_global_reference ?loc ~head (fun _ -> true) ntn sc)
let smart_global_inductive = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
| AN r ->
global_inductive_with_alias r
| ByNotation (ntn,sc) ->
destIndRef
- (Notation.interp_notation_as_global_reference ?loc isIndRef ntn sc))
+ (Notation.interp_notation_as_global_reference ?loc ~head:false isIndRef ntn sc))
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 492671fff0..d5f104b7f8 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -42,6 +42,8 @@ let wit_var =
let wit_ref = make0 "ref"
+let wit_smart_global = make0 ~dyn:(val_tag (topwit wit_ref)) "smart_global"
+
let wit_sort_family = make0 "sort_family"
let wit_constr =
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 35de3693cb..89bdd78c70 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -39,6 +39,8 @@ val wit_var : (lident, lident, Id.t) genarg_type
val wit_ref : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
+val wit_smart_global : (qualid or_by_notation, GlobRef.t located or_var, GlobRef.t) genarg_type
+
val wit_sort_family : (Sorts.family, unit, unit) genarg_type
val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 7184f5ea29..bd3e234a91 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Util
open Pp
open CErrors
open Names
@@ -82,16 +81,9 @@ let in_syntax_constant : (bool * syndef) -> obj =
subst_function = subst_syntax_constant;
classify_function = classify_syntax_constant }
-type syndef_interpretation = (Id.t * subscopes) list * notation_constr
-
-(* Coercions to the general format of notation that also supports
- variables bound to list of expressions *)
-let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,((Constrexpr.InConstrEntrySomeLevel,sc),NtnTypeConstr))) ids,ac)
-let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac)
-
let declare_syntactic_definition ~local deprecation id ~onlyparsing pat =
let syndef =
- { syndef_pattern = in_pat pat;
+ { syndef_pattern = pat;
syndef_onlyparsing = onlyparsing;
syndef_deprecation = deprecation;
}
@@ -106,14 +98,12 @@ let warn_deprecated_syntactic_definition =
let search_syntactic_definition ?loc kn =
let syndef = KNmap.find kn !syntax_table in
- let def = out_pat syndef.syndef_pattern in
Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation;
- def
+ syndef.syndef_pattern
let search_filtered_syntactic_definition ?loc filter kn =
let syndef = KNmap.find kn !syntax_table in
- let def = out_pat syndef.syndef_pattern in
- let res = filter def in
+ let res = filter syndef.syndef_pattern in
if Option.has_some res then
Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation;
res
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 8b323462a1..66a3132f2a 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -13,12 +13,10 @@ open Notation_term
(** Syntactic definitions. *)
-type syndef_interpretation = (Id.t * subscopes) list * notation_constr
-
val declare_syntactic_definition : local:bool -> Deprecation.t option -> Id.t ->
- onlyparsing:bool -> syndef_interpretation -> unit
+ onlyparsing:bool -> interpretation -> unit
-val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation
+val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> interpretation
val search_filtered_syntactic_definition : ?loc:Loc.t ->
- (syndef_interpretation -> 'a option) -> KerName.t -> 'a option
+ (interpretation -> 'a option) -> KerName.t -> 'a option
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 01:46:45 +0000