aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr.ml1
-rw-r--r--interp/constrexpr_ops.ml16
-rw-r--r--interp/constrexpr_ops.mli24
-rw-r--r--interp/constrextern.ml27
-rw-r--r--interp/constrintern.ml90
-rw-r--r--interp/constrintern.mli7
-rw-r--r--interp/declare.ml112
-rw-r--r--interp/declare.mli5
-rw-r--r--interp/discharge.ml11
-rw-r--r--interp/dumpglob.ml2
-rw-r--r--interp/genintern.ml15
-rw-r--r--interp/genintern.mli9
-rw-r--r--interp/impargs.ml20
-rw-r--r--interp/interp.mllib2
-rw-r--r--interp/notation.ml8
-rw-r--r--interp/notation_ops.ml29
-rw-r--r--interp/notation_term.ml1
-rw-r--r--interp/syntax_def.ml7
18 files changed, 212 insertions, 174 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index d8dd4ef6dd..77d612cfd9 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -114,7 +114,6 @@ and constr_expr_r =
| CGeneralization of binding_kind * abstraction_kind option * constr_expr
| CPrim of prim_token
| CDelimiters of string * constr_expr
- | CProj of qualid * constr_expr
and constr_expr = constr_expr_r CAst.t
and case_expr = constr_expr (* expression that is being matched *)
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 011c4a6e4e..d5f0b7bff6 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -177,12 +177,10 @@ let rec constr_expr_eq e1 e2 =
| CDelimiters(s1,e1), CDelimiters(s2,e2) ->
String.equal s1 s2 &&
constr_expr_eq e1 e2
- | CProj(p1,c1), CProj(p2,c2) ->
- qualid_eq p1 p2 && constr_expr_eq c1 c2
| (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _
| CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
| CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _
- | CGeneralization _ | CDelimiters _ | CProj _), _ -> false
+ | CGeneralization _ | CDelimiters _ ), _ -> false
and args_eq (a1,e1) (a2,e2) =
Option.equal (eq_ast explicitation_eq) e1 e2 &&
@@ -359,8 +357,6 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
(fold_local_binders g f n acc t lb) c lb) l acc
| CCoFix (_,_) ->
Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc
- | CProj (_,c) ->
- f n acc c
)
let free_vars_of_constr_expr c =
@@ -439,8 +435,6 @@ let map_constr_expr_with_binders g f e = CAst.map (function
let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_) -> g id e) e' dl in
let d' = f e'' d in
(id,bl',t',d')) dl)
- | CProj (p,c) ->
- CProj (p, f e c)
)
(* Used in constrintern *)
@@ -532,6 +526,14 @@ let mkAppC (f,l) =
| CApp (g,l') -> CAst.make @@ CApp (g, l' @ l)
| _ -> CAst.make @@ CApp ((None, f), l)
+let mkProdCN ?loc bll c =
+ if bll = [] then c else
+ CAst.make ?loc @@ CProdN (bll,c)
+
+let mkLambdaCN ?loc bll c =
+ if bll = [] then c else
+ CAst.make ?loc @@ CLambdaN (bll,c)
+
let mkCProdN ?loc bll c =
CAst.make ?loc @@ CProdN (bll,c)
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 61e8aa1b51..9e83bde8b2 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -38,22 +38,36 @@ val constr_loc : constr_expr -> Loc.t option
val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t option
val local_binders_loc : local_binder_expr list -> Loc.t option
-(** {6 Constructors}*)
+(** {6 Constructors} *)
+
+(** {7 Term constructors} *)
+
+(** Basic form of the corresponding constructors *)
val mkIdentC : Id.t -> constr_expr
val mkRefC : qualid -> constr_expr
-val mkAppC : constr_expr * constr_expr list -> constr_expr
val mkCastC : constr_expr * constr_expr Glob_term.cast_type -> constr_expr
val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr
val mkLetInC : lname * constr_expr * constr_expr option * constr_expr -> constr_expr
val mkProdC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr
-val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
-(** Same as [abstract_constr_expr], with location *)
+val mkAppC : constr_expr * constr_expr list -> constr_expr
+(** Basic form of application, collapsing nested applications *)
+(** Optimized constructors: does not add a constructor for an empty binder list *)
+
+val mkLambdaCN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
+val mkProdCN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
+
+(** Aliases for the corresponding constructors; generally [mkLambdaCN] and
+ [mkProdCN] should be preferred *)
+
+val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
val mkCProdN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
-(** Same as [prod_constr_expr], with location *)
+(** {7 Pattern constructors} *)
+
+(** Interpretation of a list of patterns as a disjunctive pattern (optimized) *)
val mkCPatOr : ?loc:Loc.t -> cases_pattern_expr list -> cases_pattern_expr
val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list -> cases_pattern_expr
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ddc0a5c000..838ef40545 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -26,7 +26,6 @@ open Notation_ops
open Glob_term
open Glob_ops
open Pattern
-open Nametab
open Notation
open Detyping
open Decl_kinds
@@ -102,7 +101,7 @@ let _show_inactive_notations () =
(function
| NotationRule (scopt, ntn) ->
Feedback.msg_notice (pr_notation ntn ++ show_scope scopt)
- | SynDefRule kn -> Feedback.msg_notice (str (Names.KerName.to_string kn)))
+ | SynDefRule kn -> Feedback.msg_notice (str (string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn))))
!inactive_notations_table
let deactivate_notation nr =
@@ -135,8 +134,9 @@ let reactivate_notation nr =
++ str "is already active" ++ show_scope scopt ++
str ".")
| SynDefRule kn ->
+ let s = string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) in
Feedback.msg_warning
- (str "Notation" ++ spc () ++ str (Names.KerName.to_string kn)
+ (str "Notation" ++ spc () ++ str s
++ spc () ++ str "is already active.")
@@ -212,7 +212,7 @@ let is_record indsp =
with Not_found -> false
let encode_record r =
- let indsp = global_inductive r in
+ let indsp = Nametab.global_inductive r in
if not (is_record indsp) then
user_err ?loc:r.CAst.loc ~hdr:"encode_record"
(str "This type is not a structure type.");
@@ -278,7 +278,7 @@ let extern_evar n l = CEvar (n,l)
may be inaccurate *)
let default_extern_reference ?loc vars r =
- shortest_qualid_of_global ?loc vars r
+ Nametab.shortest_qualid_of_global ?loc vars r
let my_extern_reference = ref default_extern_reference
@@ -480,7 +480,10 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
(make_pat_notation ?loc ntn (l,ll) l2') key)
end
| SynDefRule kn ->
- let qid = shortest_qualid_of_syndef ?loc vars kn in
+ match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
+ let qid = Nametab.shortest_qualid_of_syndef ?loc vars kn in
let l1 =
List.rev_map (fun (c,(subentry,(scopt,scl))) ->
extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c)
@@ -493,7 +496,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
|None -> raise No_match
in
assert (List.is_empty substlist);
- mkPat ?loc qid (List.rev_append l1 l2')
+ insert_pat_coercion ?loc coercion (mkPat ?loc qid (List.rev_append l1 l2'))
and extern_notation_pattern allscopes vars t = function
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
@@ -957,9 +960,6 @@ let rec extern inctx scopes vars r =
| GCast (c, c') ->
CCast (sub_extern true scopes vars c,
map_cast_type (extern_typ scopes vars) c')
- | GProj (p, c) ->
- let pr = extern_reference ?loc Id.Set.empty (ConstRef (Projection.constant p)) in
- CProj (pr, sub_extern inctx scopes vars c)
in insert_coercion coercion (CAst.make ?loc c)
@@ -1134,12 +1134,15 @@ and extern_notation (custom,scopes as allscopes) vars t = function
binderlists in
insert_coercion coercion (insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key))
| SynDefRule kn ->
+ match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
let l =
List.map (fun (c,(subentry,(scopt,scl))) ->
extern true (subentry,(scopt,scl@snd scopes)) vars c, None)
terms in
- let a = CRef (shortest_qualid_of_syndef ?loc vars kn,None) in
- CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in
+ let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in
+ insert_coercion coercion (CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l)) in
if List.is_empty args then e
else
let args = fill_arg_scopes args argsscopes allscopes in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1c8d957014..02db8f6aab 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -28,7 +28,6 @@ open Constrexpr
open Constrexpr_ops
open Notation_term
open Notation_ops
-open Nametab
open Notation
open Inductiveops
open Decl_kinds
@@ -121,6 +120,9 @@ type internalization_error =
| UnboundFixName of bool * Id.t
| NonLinearPattern of Id.t
| BadPatternsNumber of int * int
+ | NotAProjection of qualid
+ | NotAProjectionOf of qualid * qualid
+ | ProjectionsOfDifferentRecords of qualid * qualid
exception InternalizationError of internalization_error Loc.located
@@ -146,6 +148,16 @@ let explain_bad_patterns_number n1 n2 =
str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++
str " but found " ++ int n2
+let explain_field_not_a_projection field_id =
+ pr_qualid field_id ++ str ": Not a projection"
+
+let explain_field_not_a_projection_of field_id inductive_id =
+ pr_qualid field_id ++ str ": Not a projection of inductive " ++ pr_qualid inductive_id
+
+let explain_projections_of_diff_records inductive1_id inductive2_id =
+ str "This record contains fields of both " ++ pr_qualid inductive1_id ++
+ str " and " ++ pr_qualid inductive2_id
+
let explain_internalization_error e =
let pp = match e with
| VariableCapture (id,id') -> explain_variable_capture id id'
@@ -154,6 +166,11 @@ let explain_internalization_error e =
| UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id
| NonLinearPattern id -> explain_non_linear_pattern id
| BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2
+ | NotAProjection field_id -> explain_field_not_a_projection field_id
+ | NotAProjectionOf (field_id, inductive_id) ->
+ explain_field_not_a_projection_of field_id inductive_id
+ | ProjectionsOfDifferentRecords (inductive1_id, inductive2_id) ->
+ explain_projections_of_diff_records inductive1_id inductive2_id
in pp ++ str "."
let error_bad_inductive_type ?loc =
@@ -633,7 +650,7 @@ let terms_of_binders bl =
| PatVar (Name id) -> CRef (qualid_of_ident id, None)
| PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc ()
| PatCstr (c,l,_) ->
- let qid = qualid_of_path ?loc (path_of_global (ConstructRef c)) in
+ let qid = qualid_of_path ?loc (Nametab.path_of_global (ConstructRef c)) in
let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in
let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in
@@ -720,8 +737,8 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
try
let gc = intern nenv c in
- Id.Map.add id (gc, Some c) map
- with GlobalizationError _ -> map
+ Id.Map.add id (gc, None) map
+ with Nametab.GlobalizationError _ -> map
in
let mk_env' (c, (onlyident,(tmp_scope,subscopes))) =
let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
@@ -986,7 +1003,7 @@ let intern_extended_global_of_qualid qid =
let intern_reference qid =
let r =
try intern_extended_global_of_qualid qid
- with Not_found -> error_global_not_found qid
+ with Not_found -> Nametab.error_global_not_found qid
in
Smartlocate.global_of_extended_global r
@@ -1058,11 +1075,11 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args qi
(* Extra allowance for non globalizing functions *)
if !interning_grammar || env.unb then
(gvar (loc,qualid_basename qid) us, [], [], []), args
- else error_global_not_found qid
+ else Nametab.error_global_not_found qid
else
let r,projapp,args2 =
try intern_qualid qid intern env ntnvars us args
- with Not_found -> error_global_not_found qid
+ with Not_found -> Nametab.error_global_not_found qid
in
let x, imp, scopes, l = find_appl_head_data r in
(x,imp,scopes,l), args2
@@ -1282,6 +1299,10 @@ let check_duplicate loc fields =
user_err ?loc (str "This record defines several times the field " ++
pr_qualid r ++ str ".")
+let inductive_of_record loc record =
+ let inductive = IndRef (inductive_of_constructor record.Recordops.s_CONST) in
+ Nametab.shortest_qualid_of_global ?loc Id.Set.empty inductive
+
(** [sort_fields ~complete loc fields completer] expects a list
[fields] of field assignments [f = e1; g = e2; ...], where [f, g]
are fields of a record and [e1] are "values" (either terms, when
@@ -1304,15 +1325,14 @@ let sort_fields ~complete loc fields completer =
let gr = global_reference_of_reference first_field_ref in
(gr, Recordops.find_projection gr)
with Not_found ->
- user_err ?loc ~hdr:"intern"
- (pr_qualid first_field_ref ++ str": Not a projection")
+ raise (InternalizationError(loc, NotAProjection first_field_ref))
in
(* the number of parameters *)
let nparams = record.Recordops.s_EXPECTEDPARAM in
(* the reference constructor of the record *)
let base_constructor =
let global_record_id = ConstructRef record.Recordops.s_CONST in
- try shortest_qualid_of_global ?loc Id.Set.empty global_record_id
+ try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id
with Not_found ->
anomaly (str "Environment corruption for records.") in
let () = check_duplicate loc fields in
@@ -1364,12 +1384,18 @@ let sort_fields ~complete loc fields completer =
with Not_found ->
user_err ?loc ~hdr:"intern"
(str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in
+ let this_field_record = try Recordops.find_projection field_glob_ref
+ with Not_found ->
+ let inductive_ref = inductive_of_record loc record in
+ raise (InternalizationError(loc, NotAProjectionOf (field_ref, inductive_ref)))
+ in
let remaining_projs, (field_index, _) =
let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in
try CList.extract_first the_proj remaining_projs
with Not_found ->
- user_err ?loc
- (str "This record contains fields of different records.")
+ let ind1 = inductive_of_record loc record in
+ let ind2 = inductive_of_record loc this_field_record in
+ raise (InternalizationError(loc, ProjectionsOfDifferentRecords (ind1, ind2)))
in
index_fields fields remaining_projs ((field_index, field_value) :: acc)
| [] ->
@@ -1493,7 +1519,7 @@ let drop_notations_pattern looked_for genv =
in
let rec drop_syndef top scopes qid pats =
try
- match locate_extended qid with
+ match Nametab.locate_extended qid with
| SynDef sp ->
let (vars,a) = Syntax_def.search_syntactic_definition sp in
(match a with
@@ -1550,7 +1576,7 @@ let drop_notations_pattern looked_for genv =
| None -> raise (InternalizationError (loc,NotAConstructor head))
end
| CPatCstr (qid, Some expl_pl, pl) ->
- let g = try locate qid
+ let g = try Nametab.locate qid
with Not_found ->
raise (InternalizationError (loc,NotAConstructor qid)) in
if expl_pl == [] then
@@ -1863,12 +1889,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
Array.map (fun (bl,_,_) -> bl) idl,
Array.map (fun (_,ty,_) -> ty) idl,
Array.map (fun (_,_,bd) -> bd) idl)
+ | CProdN ([],c2) -> anomaly (Pp.str "The AST is malformed, found prod without binders.")
| CProdN (bl,c2) ->
let (env',bl) = List.fold_left intern_local_binder (env,[]) bl in
expand_binders ?loc mkGProd bl (intern_type env' c2)
- | CLambdaN ([],c2) ->
- (* Such a term is built sometimes: it should not change scope *)
- intern env c2
+ | CLambdaN ([],c2) -> anomaly (Pp.str "The AST is malformed, found lambda without binders.")
| CLambdaN (bl,c2) ->
let (env',bl) = List.fold_left intern_local_binder (reset_tmp_scope env,[]) bl in
expand_binders ?loc mkGLambda bl (intern env' c2)
@@ -2026,15 +2051,22 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let (ltacvars, ntnvars) = lvar in
(* Preventively declare notation variables in ltac as non-bindings *)
Id.Map.iter (fun x (used_as_binder,_,_) -> used_as_binder := false) ntnvars;
- let ntnvars = Id.Map.domain ntnvars in
let extra = ltacvars.ltac_extra in
+ (* We inform ltac that the interning vars and the notation vars are bound *)
+ (* but we could instead rely on the "intern_sign" *)
let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in
- let lvars = Id.Set.union lvars ntnvars in
+ let lvars = Id.Set.union lvars (Id.Map.domain ntnvars) in
let ltacvars = Id.Set.union lvars env.ids in
+ (* Propagating enough information for mutual interning with tac-in-term *)
+ let intern_sign = {
+ Genintern.intern_ids = env.ids;
+ Genintern.notation_variable_status = ntnvars
+ } in
let ist = {
Genintern.genv = globalenv;
ltacvars;
extra;
+ intern_sign;
} in
let (_, glb) = Genintern.generic_intern ist gen in
Some glb
@@ -2062,13 +2094,6 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| CCast (c1, c2) ->
DAst.make ?loc @@
GCast (intern env c1, map_cast_type (intern_type env) c2)
- | CProj (pr, c) ->
- match intern_reference pr with
- | ConstRef p ->
- let p = Option.get @@ Recordops.find_primitive_projection p in
- DAst.make ?loc @@ GProj (Projection.make p false, intern env c)
- | _ ->
- raise (InternalizationError (loc,IllegalMetavariable)) (* FIXME *)
)
and intern_type env = intern (set_type_scope env)
@@ -2326,16 +2351,23 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign)
~pattern_mode:true ~ltacvars env sigma c in
pattern_of_glob_constr c
+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 impls = empty_internalization_env in
+ internalize env {ids; unb = false; tmp_scope; scopes = []; impls}
+ pattern_mode (ltacvars, vl) c
+
let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
+ let ids = extract_ids env in
(* [vl] is intended to remember the scope of the free variables of [a] *)
let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in
let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in
- let c = internalize (Global.env()) {ids = extract_ids env; unb = false;
- tmp_scope = None; scopes = []; impls = impls}
+ let c = internalize env {ids; unb = false; tmp_scope = None; scopes = []; impls}
false (empty_ltac_sign, vl) a in
+ (* Splits variables into those that are binding, bound, or both *)
(* Translate and check that [c] has all its free variables bound in [vars] *)
let a, reversible = notation_constr_of_glob_constr nenv c in
- (* Splits variables into those that are binding, bound, or both *)
(* binding and bound *)
let out_scope = function None -> None,[] | Some (a,l) -> a,l in
let unused = match reversible with NonInjective ids -> ids | _ -> [] in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index dd0944cc48..147a903fe2 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -185,6 +185,13 @@ val interp_notation_constr : env -> ?impls:internalization_env ->
notation_interp_env -> constr_expr ->
(bool * subscopes) Id.Map.t * notation_constr * reversibility_status
+(** Idem but to glob_constr (weaker check of binders) *)
+
+val intern_core : typing_constraint ->
+ env -> evar_map -> ?pattern_mode:bool -> ?ltacvars:ltac_sign ->
+ Genintern.intern_variable_status -> constr_expr ->
+ glob_constr
+
(** Globalization options *)
val parsing_explicit : bool ref
diff --git a/interp/declare.ml b/interp/declare.ml
index 22e6cf9d1c..7a32018c0e 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -60,14 +60,7 @@ let open_constant i ((sp,kn), obj) =
if obj.cst_locl then ()
else
let con = Global.constant_of_delta_kn kn in
- Nametab.push (Nametab.Exactly i) sp (ConstRef con);
- match (Global.lookup_constant con).const_body with
- | (Def _ | Undef _) -> ()
- | OpaqueDef lc ->
- match Opaqueproof.get_constraints (Global.opaque_tables ()) lc with
- | Some f when Future.is_val f ->
- Global.push_context_set false (Future.force f)
- | _ -> ()
+ Nametab.push (Nametab.Exactly i) sp (ConstRef con)
let exists_name id =
variable_exists id || Global.exists_objlabel (Label.of_id id)
@@ -78,7 +71,6 @@ let check_exists sp =
let cache_constant ((sp,kn), obj) =
let id = basename sp in
- let _,dir,_ = KerName.repr kn in
let kn' =
match obj.cst_decl with
| None ->
@@ -87,7 +79,7 @@ let cache_constant ((sp,kn), obj) =
else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
| Some decl ->
let () = check_exists sp in
- Global.add_constant dir id decl
+ Global.add_constant ~in_section:(Lib.sections_are_opened ()) id decl
in
assert (Constant.equal kn' (Constant.make1 kn));
Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn));
@@ -136,7 +128,7 @@ let register_side_effect (c, role) =
cst_kind = IsProof Theorem;
cst_locl = false;
} in
- let id = Label.to_id (pi3 (Constant.repr3 c)) in
+ let id = Label.to_id (Constant.label c) in
ignore(add_leaf id o);
update_tables c;
match role with
@@ -311,8 +303,7 @@ let cache_inductive ((sp,kn),mie) =
let names = inductive_names sp kn mie in
List.iter check_exists (List.map fst names);
let id = basename sp in
- let _,dir,_ = KerName.repr kn in
- let kn' = Global.add_mind dir id mie in
+ let kn' = Global.add_mind id mie in
assert (MutInd.equal kn' (MutInd.make1 kn));
let mind = Global.lookup_mind kn' in
add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
@@ -479,21 +470,7 @@ type universe_source =
| QualifiedUniv of Id.t (* global universe introduced by some global value *)
| UnqualifiedUniv (* other global universe *)
-type universe_decl = universe_source * Nametab.universe_id
-
-let add_universe src (dp, i) =
- let level = Univ.Level.make dp i in
- let optpoly = match src with
- | BoundUniv -> Some true
- | UnqualifiedUniv -> Some false
- | QualifiedUniv _ -> None
- in
- Option.iter (fun poly ->
- let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
- Global.push_context_set poly ctx;
- UnivNames.add_global_universe level poly;
- if poly then Lib.add_section_context ctx)
- optpoly
+type universe_name_decl = universe_source * (Id.t * Nametab.universe_id) list
let check_exists sp =
let depth = sections_depth () in
@@ -502,41 +479,42 @@ let check_exists sp =
alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists")
else ()
-let qualify_univ src (sp,i as orig) =
+let qualify_univ i sp src id =
+ let open Libnames in
match src with
- | BoundUniv | UnqualifiedUniv -> orig
+ | BoundUniv | UnqualifiedUniv ->
+ let sp = dirpath sp in
+ i, make_path sp id
| QualifiedUniv l ->
- let sp0, id = Libnames.repr_path sp in
- let sp0 = DirPath.repr sp0 in
- Libnames.make_path (DirPath.make (l::sp0)) id, i+1
-
-let cache_universe ((sp, _), (src, id)) =
- let sp, i = qualify_univ src (sp,1) in
- let () = check_exists sp in
- let () = Nametab.push_universe (Nametab.Until i) sp id in
- add_universe src id
-
-let load_universe i ((sp, _), (src, id)) =
- let sp, i = qualify_univ src (sp,i) in
- let () = Nametab.push_universe (Nametab.Until i) sp id in
- add_universe src id
-
-let open_universe i ((sp, _), (src, id)) =
- let sp, i = qualify_univ src (sp,i) in
- let () = Nametab.push_universe (Nametab.Exactly i) sp id in
- ()
-
-let discharge_universe = function
+ let sp = dirpath sp in
+ let sp = DirPath.repr sp in
+ Nametab.map_visibility succ i, make_path (DirPath.make (l::sp)) id
+
+let do_univ_name ~check i sp src (id,univ) =
+ let i, sp = qualify_univ i sp src id in
+ if check then check_exists sp;
+ Nametab.push_universe i sp univ
+
+let cache_univ_names ((sp, _), (src, univs)) =
+ List.iter (do_univ_name ~check:true (Nametab.Until 1) sp src) univs
+
+let load_univ_names i ((sp, _), (src, univs)) =
+ List.iter (do_univ_name ~check:false (Nametab.Until i) sp src) univs
+
+let open_univ_names i ((sp, _), (src, univs)) =
+ List.iter (do_univ_name ~check:false (Nametab.Exactly i) sp src) univs
+
+let discharge_univ_names = function
| _, (BoundUniv, _) -> None
| _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x
-let input_universe : universe_decl -> Libobject.obj =
+let input_univ_names : universe_name_decl -> Libobject.obj =
declare_object
{ (default_object "Global universe name state") with
- cache_function = cache_universe;
- load_function = load_universe;
- open_function = open_universe;
- discharge_function = discharge_universe;
+ cache_function = cache_univ_names;
+ load_function = load_univ_names;
+ open_function = open_univ_names;
+ discharge_function = discharge_univ_names;
subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a);
classify_function = (fun a -> Substitute a) }
@@ -552,12 +530,12 @@ let declare_univ_binders gr pl =
anomaly ~label:"declare_univ_binders"
Pp.(str "declare_univ_binders on an constructor reference")
in
- Id.Map.iter (fun id lvl ->
- match Univ.Level.name lvl with
- | None -> ()
- | Some na ->
- ignore (Lib.add_leaf id (input_universe (QualifiedUniv l, na))))
- pl
+ let univs = Id.Map.fold (fun id univ univs ->
+ match Univ.Level.name univ with
+ | None -> assert false (* having Prop/Set/Var as binders is nonsense *)
+ | Some univ -> (id,univ)::univs) pl []
+ in
+ Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
let do_universe poly l =
let in_section = Lib.sections_are_opened () in
@@ -571,16 +549,18 @@ let do_universe poly l =
let lev = UnivGen.new_univ_id () in
(id, lev)) l
in
+ let ctx = List.fold_left (fun ctx (_,(dp,i)) -> Univ.LSet.add (Univ.Level.make dp i) ctx)
+ Univ.LSet.empty l, Univ.Constraint.empty
+ in
+ let () = declare_universe_context poly ctx in
let src = if poly then BoundUniv else UnqualifiedUniv in
- List.iter (fun (id,lev) ->
- ignore(Lib.add_leaf id (input_universe (src, lev))))
- l
+ Lib.add_anonymous_leaf (input_univ_names (src, l))
let do_constraint poly l =
let open Univ in
let u_of_id x =
let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in
- UnivNames.is_polymorphic level, level
+ Lib.is_polymorphic_univ level, level
in
let in_section = Lib.sections_are_opened () in
let () =
diff --git a/interp/declare.mli b/interp/declare.mli
index 02e73cd66c..468e056909 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
-open Libnames
open Constr
open Entries
open Decl_kinds
@@ -29,7 +28,7 @@ type section_variable_entry =
type variable_declaration = DirPath.t * section_variable_entry * logical_kind
-val declare_variable : variable -> variable_declaration -> object_name
+val declare_variable : variable -> variable_declaration -> Libobject.object_name
(** Declaration of global constructions
i.e. Definition/Theorem/Axiom/Parameter/... *)
@@ -69,7 +68,7 @@ val set_declare_scheme :
(** [declare_mind me] declares a block of inductive types with
their constructors in the current section; it returns the path of
the whole block and a boolean indicating if it is a primitive record. *)
-val declare_mind : mutual_inductive_entry -> object_name * bool
+val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool
(** Declaration messages *)
diff --git a/interp/discharge.ml b/interp/discharge.ml
index 0e44a8b467..21b2e85e8f 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -8,8 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Names
-open CErrors
open Util
open Term
open Constr
@@ -17,17 +15,10 @@ open Vars
open Declarations
open Cooking
open Entries
-open Context.Rel.Declaration
(********************************)
(* Discharging mutual inductive *)
-let detype_param =
- function
- | LocalAssum (Name id, p) -> id, LocalAssumEntry p
- | LocalDef (Name id, p,_) -> id, LocalDefEntry p
- | _ -> anomaly (Pp.str "Unnamed inductive local variable.")
-
(* Replace
Var(y1)..Var(yq):C1..Cq |- Ij:Bj
@@ -57,7 +48,7 @@ let abstract_inductive decls nparamdecls inds =
(* To be sure to be the same as before, should probably be moved to process_inductive *)
let params' = let (_,arity,_,_,_) = List.hd inds' in
let (params,_) = decompose_prod_n_assum nparamdecls' arity in
- List.map detype_param params
+ params
in
let ind'' =
List.map
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index ccad6b19eb..f5be0ddbae 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -234,7 +234,7 @@ let add_glob ?loc ref =
add_glob_gen ?loc sp lib_dp ty
let mp_of_kn kn =
- let mp,sec,l = Names.KerName.repr kn in
+ let mp,l = Names.KerName.repr kn in
Names.MPdot (mp,l)
let add_glob_kn ?loc kn =
diff --git a/interp/genintern.ml b/interp/genintern.ml
index d9a0db040a..1b736b7977 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -14,16 +14,31 @@ open Genarg
module Store = Store.Make ()
+type intern_variable_status = {
+ intern_ids : Id.Set.t;
+ notation_variable_status :
+ (bool ref * Notation_term.subscopes option ref *
+ Notation_term.notation_var_internalization_type)
+ Id.Map.t
+}
+
type glob_sign = {
ltacvars : Id.Set.t;
genv : Environ.env;
extra : Store.t;
+ intern_sign : intern_variable_status;
+}
+
+let empty_intern_sign = {
+ intern_ids = Id.Set.empty;
+ notation_variable_status = Id.Map.empty;
}
let empty_glob_sign env = {
ltacvars = Id.Set.empty;
genv = env;
extra = Store.empty;
+ intern_sign = empty_intern_sign;
}
(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
diff --git a/interp/genintern.mli b/interp/genintern.mli
index f4f064bcac..4100f39029 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -14,10 +14,19 @@ open Genarg
module Store : Store.S
+type intern_variable_status = {
+ intern_ids : Id.Set.t;
+ notation_variable_status :
+ (bool ref * Notation_term.subscopes option ref *
+ Notation_term.notation_var_internalization_type)
+ Id.Map.t
+}
+
type glob_sign = {
ltacvars : Id.Set.t;
genv : Environ.env;
extra : Store.t;
+ intern_sign : intern_variable_status;
}
val empty_glob_sign : Environ.env -> glob_sign
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 3603367cf1..d8582d856e 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -450,13 +450,13 @@ let compute_mib_implicits flags kn =
(Array.mapi (* No need to lift, arities contain no de Bruijn *)
(fun i mip ->
(** No need to care about constraints here *)
- let ty, _ = Global.type_of_global_in_context env (IndRef (kn,i)) in
+ let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in
Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty))
mib.mind_packets) in
let env_ar = Environ.push_rel_context ar env in
let imps_one_inductive i mip =
let ind = (kn,i) in
- let ar, _ = Global.type_of_global_in_context env (IndRef ind) in
+ let ar, _ = Typeops.type_of_global_in_context env (IndRef ind) in
((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)),
Array.mapi (fun j c ->
(ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c))
@@ -561,29 +561,27 @@ let discharge_implicits (_,(req,l)) =
| ImplInteractive (ref,flags,exp) ->
(try
let vars = variable_section_segment_of_reference ref in
- let ref' = if isVarRef ref then ref else pop_global_reference ref in
let extra_impls = impls_of_context vars in
- let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
- Some (ImplInteractive (ref',flags,exp),l')
+ let l' = [ref, List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
+ Some (ImplInteractive (ref,flags,exp),l')
with Not_found -> (* ref not defined in this section *) Some (req,l))
| ImplConstant (con,flags) ->
(try
- let con' = pop_con con in
let vars = variable_section_segment_of_reference (ConstRef con) in
let extra_impls = impls_of_context vars in
let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in
- let l' = [ConstRef con',newimpls] in
- Some (ImplConstant (con',flags),l')
+ let l' = [ConstRef con,newimpls] in
+ Some (ImplConstant (con,flags),l')
with Not_found -> (* con not defined in this section *) Some (req,l))
| ImplMutualInductive (kn,flags) ->
(try
let l' = List.map (fun (gr, l) ->
let vars = variable_section_segment_of_reference gr in
let extra_impls = impls_of_context vars in
- ((if isVarRef gr then gr else pop_global_reference gr),
+ (gr,
List.map (add_section_impls vars extra_impls) l)) l
in
- Some (ImplMutualInductive (pop_kn kn,flags),l')
+ Some (ImplMutualInductive (kn,flags),l')
with Not_found -> (* ref not defined in this section *) Some (req,l))
let rebuild_implicits (req,l) =
@@ -696,7 +694,7 @@ let declare_manual_implicits local ref ?enriching l =
let flags = !implicit_args in
let env = Global.env () in
let sigma = Evd.from_env env in
- let t, _ = Global.type_of_global_in_context env ref in
+ let t, _ = Typeops.type_of_global_in_context env ref in
let t = of_constr t in
let enriching = Option.default flags.auto enriching in
let autoimpls = compute_auto_implicits env sigma flags enriching t in
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 3668455aeb..aa20bda705 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -3,8 +3,8 @@ Genredexpr
Redops
Tactypes
Stdarg
-Genintern
Notation_term
+Genintern
Notation_ops
Notation
Syntax_def
diff --git a/interp/notation.ml b/interp/notation.ml
index 02c7812e21..db8ee5bc18 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1304,7 +1304,7 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) =
vars |> List.map fst |> List.filter is_local_assum |> List.length
with
Not_found (* Not a ref defined in this section *) -> 0 in
- Some (req,Lib.discharge_global r,n,l,[])
+ Some (req,r,n,l,[])
let classify_arguments_scope (req,_,_,_,_ as obj) =
if req == ArgsScopeNoDischarge then Dispose else Substitute obj
@@ -1314,7 +1314,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
| ArgsScopeNoDischarge -> assert false
| ArgsScopeAuto ->
let env = Global.env () in (*FIXME?*)
- let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in
+ 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
(req,r,List.length scs,scs,cls)
| ArgsScopeManual ->
@@ -1322,7 +1322,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
for the extra parameters of the section. Discard the classes
of the manually given scopes to avoid further re-computations. *)
let env = Global.env () in (*FIXME?*)
- let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in
+ 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 l1 = List.firstn n l' in
let cls1 = List.firstn n cls in
@@ -1369,7 +1369,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 @@ Global.type_of_global_in_context env ref in
+ 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
declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 06943ce7b9..7a525f84a5 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -89,11 +89,9 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
glob_sort_eq s1 s2
| NCast (t1, c1), NCast (t2, c2) ->
(eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2
-| NProj (p1, c1), NProj (p2, c2) ->
- Projection.equal p1 p2 && eq_notation_constr vars c1 c2
| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
| NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
- | NRec _ | NSort _ | NCast _ | NProj _), _ -> false
+ | NRec _ | NSort _ | NCast _ ), _ -> false
(**********************************************************************)
(* Re-interpret a notation as a glob_constr, taking care of binders *)
@@ -155,11 +153,13 @@ let protect g e na =
if disjpat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern.");
e',na
-let apply_cases_pattern ?loc ((ids,disjpat),id) c =
- let tm = DAst.make ?loc (GVar id) in
+let apply_cases_pattern_term ?loc (ids,disjpat) tm c =
let eqns = List.map (fun pat -> (CAst.make ?loc (ids,[pat],c))) disjpat in
DAst.make ?loc @@ GCases (Constr.LetPatternStyle, None, [tm,(Anonymous,None)], eqns)
+let apply_cases_pattern ?loc (ids_disjpat,id) c =
+ apply_cases_pattern_term ?loc ids_disjpat (DAst.make ?loc (GVar id)) c
+
let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
let lt x = DAst.make ?loc x in lt @@ match nc with
| NVar id -> GVar id
@@ -184,7 +184,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
let e',disjpat,na = g e na in
(match disjpat with
| None -> GLetIn (na,f e b,Option.map (f e) t,f e' c)
- | Some disjpat -> DAst.get (apply_cases_pattern ?loc disjpat (f e' c)))
+ | Some (disjpat,_id) -> DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c)))
| NCases (sty,rtntypopt,tml,eqnl) ->
let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
let e',t' = match t with
@@ -220,7 +220,6 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
| NSort x -> GSort x
| NHole (x, naming, arg) -> GHole (x, naming, arg)
| NRef x -> GRef (x,None)
- | NProj (p,c) -> GProj (p, f e c)
let glob_constr_of_notation_constr ?loc x =
let rec aux () x =
@@ -440,7 +439,6 @@ let notation_constr_and_vars_of_glob_constr recvars a =
if arg != None then has_ltac := true;
NHole (w, naming, arg)
| GRef (r,_) -> NRef r
- | GProj (p, c) -> NProj (p, aux c)
| GEvar _ | GPatVar _ ->
user_err Pp.(str "Existential variables not allowed in notations.")
) x
@@ -640,12 +638,6 @@ let rec subst_notation_constr subst bound raw =
let k' = smartmap_cast_type (subst_notation_constr subst bound) k in
if r1' == r1 && k' == k then raw else NCast(r1',k')
- | NProj (p, c) ->
- let p' = subst_proj subst p in
- let c' = subst_notation_constr subst bound c in
- if p' == p && c' == c then raw else NProj(p', c')
-
-
let subst_interpretation subst (metas,pat) =
let bound = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty metas in
(metas,subst_notation_constr subst bound pat)
@@ -900,7 +892,9 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
| GVar id' ->
(if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
sigma
- | _ -> anomaly (str "A term which can be a binder has to be a variable.")
+ | t ->
+ (* The term is a non-variable pattern *)
+ raise No_match
with Not_found ->
(* The matching against a term allowing to find the instance has not been found yet *)
(* If it will be a different name, we shall unfortunately fail *)
@@ -1218,12 +1212,9 @@ let rec match_ inner u alp metas sigma a1 a2 =
match_names metas (alp,sigma) (Name id') na in
match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2
- | GProj(p1, t1), NProj(p2, t2) when Projection.equal p1 p2 ->
- match_in u alp metas sigma t1 t2
-
| (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
| GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
- | GCast _ | GProj _ ), _ -> raise No_match
+ | GCast _ ), _ -> raise No_match
and match_in u = match_ true u
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 942ea5ff3f..5fb0ca1b43 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -43,7 +43,6 @@ type notation_constr =
notation_constr array * notation_constr array
| NSort of glob_sort
| NCast of notation_constr * notation_constr cast_type
- | NProj of Projection.t * notation_constr
(** Note concerning NList: first constr is iterator, second is terminator;
first id is where each argument of the list has to be substituted
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index e3d490a1ad..b73d238c22 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -15,7 +15,6 @@ open Names
open Libnames
open Libobject
open Lib
-open Nametab
open Notation_term
(* Syntactic definitions. *)
@@ -38,7 +37,7 @@ let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
let is_alias_of_already_visible_name sp = function
| _,NRef ref ->
- let (dir,id) = repr_qualid (shortest_qualid_of_global Id.Set.empty ref) in
+ let (dir,id) = repr_qualid (Nametab.shortest_qualid_of_global Id.Set.empty ref) in
DirPath.is_empty dir && Id.equal id (basename sp)
| _ ->
false
@@ -83,11 +82,11 @@ let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac)
let declare_syntactic_definition local id onlyparse pat =
let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
-let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn)
+let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn)
let pr_compat_warning (kn, def, v) =
let pp_def = match def with
- | [], NRef r -> spc () ++ str "is" ++ spc () ++ pr_global_env Id.Set.empty r
+ | [], NRef r -> spc () ++ str "is" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r
| _ -> strbrk " is a compatibility notation"
in
pr_syndef kn ++ pp_def
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 02:31:32 +0000