aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/attributes.ml4
-rw-r--r--vernac/attributes.mli3
-rw-r--r--vernac/canonical.ml8
-rw-r--r--vernac/classes.ml2
-rw-r--r--vernac/comAssumption.ml6
-rw-r--r--vernac/comCoercion.ml (renamed from vernac/class.ml)4
-rw-r--r--vernac/comCoercion.mli (renamed from vernac/class.mli)2
-rw-r--r--vernac/comInductive.ml46
-rw-r--r--vernac/comInductive.mli40
-rw-r--r--vernac/declaremods.ml22
-rw-r--r--vernac/egramcoq.ml16
-rw-r--r--vernac/egramcoq.mli3
-rw-r--r--vernac/g_vernac.mlg5
-rw-r--r--vernac/himsg.ml5
-rw-r--r--vernac/library.ml66
-rw-r--r--vernac/metasyntax.ml15
-rw-r--r--vernac/ppvernac.ml4
-rw-r--r--vernac/prettyp.ml22
-rw-r--r--vernac/prettyp.mli4
-rw-r--r--vernac/record.ml15
-rw-r--r--vernac/vernac.mllib2
-rw-r--r--vernac/vernacentries.ml39
-rw-r--r--vernac/vernacexpr.ml2
23 files changed, 181 insertions, 154 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index b7a3b002bd..68d2c3a00d 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -234,5 +234,7 @@ let only_polymorphism atts = parse polymorphic atts
let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty]
let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty]
-let canonical =
+let canonical_field =
enable_attribute ~key:"canonical" ~default:(fun () -> true)
+let canonical_instance =
+ enable_attribute ~key:"canonical" ~default:(fun () -> false)
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 34ff15ca7d..0074db66d3 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -48,7 +48,8 @@ val program : bool attribute
val template : bool option attribute
val locality : bool option attribute
val deprecation : Deprecation.t option attribute
-val canonical : bool attribute
+val canonical_field : bool attribute
+val canonical_instance : bool attribute
val program_mode_option_name : string list
(** For internal use when messing with the global option. *)
diff --git a/vernac/canonical.ml b/vernac/canonical.ml
index 141b02ef63..e41610b532 100644
--- a/vernac/canonical.ml
+++ b/vernac/canonical.ml
@@ -21,10 +21,12 @@ let cache_canonical_structure (_, (o,_)) =
let sigma = Evd.from_env env in
register_canonical_structure ~warn:true env sigma o
-let discharge_canonical_structure (_,(x, local)) =
- if local then None else Some (x, local)
+let discharge_canonical_structure (_,((gref, _ as x), local)) =
+ if local || (Globnames.isVarRef gref && Lib.is_in_section gref) then None
+ else Some (x, local)
-let inCanonStruc : (Constant.t * inductive) * bool -> obj =
+
+let inCanonStruc : (GlobRef.t * inductive) * bool -> obj =
declare_object {(default_object "CANONICAL-STRUCTURE") with
open_function = open_canonical_structure;
cache_function = cache_canonical_structure;
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 0333b73ffe..c9b5144299 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -410,7 +410,7 @@ let do_instance_resolve_TC termtype sigma env =
(* Beware of this step, it is required as to minimize universes. *)
let sigma = Evd.minimize_universes sigma in
(* Check that the type is free of evars now. *)
- Pretyping.check_evars env (Evd.from_env env) sigma termtype;
+ Pretyping.check_evars env sigma termtype;
termtype, sigma
let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst =
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index a001420f74..625ffb5a06 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -32,7 +32,7 @@ let declare_variable is_coe ~kind typ imps impl {CAst.v=name} =
let env = Global.env () in
let sigma = Evd.from_env env in
let () = Classes.declare_instance env sigma None true r in
- let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in
+ let () = if is_coe then ComCoercion.try_add_new_coercion r ~local:true ~poly:false in
()
let instance_of_univ_entry = function
@@ -65,7 +65,7 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name
| Declare.ImportNeedQualified -> true
| Declare.ImportDefaultBehavior -> false
in
- let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in
+ let () = if is_coe then ComCoercion.try_add_new_coercion gr ~local ~poly in
let inst = instance_of_univ_entry univs in
(gr,inst)
@@ -255,7 +255,7 @@ let context ~poly l =
let sigma, (_, ((_env, ctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
(* Note, we must use the normalized evar from now on! *)
let sigma = Evd.minimize_universes sigma in
- let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in
+ let ce t = Pretyping.check_evars env sigma t in
let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) ctx in
(* reorder, evar-normalize and add implicit status *)
let ctx = List.rev_map (fun d ->
diff --git a/vernac/class.ml b/vernac/comCoercion.ml
index 3c43b125d1..56ab6f289d 100644
--- a/vernac/class.ml
+++ b/vernac/comCoercion.ml
@@ -18,7 +18,7 @@ open Context
open Vars
open Termops
open Environ
-open Classops
+open Coercionops
open Declare
open Libobject
@@ -231,7 +231,7 @@ let check_source = function
let cache_coercion (_,c) =
let env = Global.env () in
let sigma = Evd.from_env env in
- Classops.declare_coercion env sigma c
+ Coercionops.declare_coercion env sigma c
let open_coercion i o =
if Int.equal i 1 then
diff --git a/vernac/class.mli b/vernac/comCoercion.mli
index 3254d5d981..f98ef4fdd6 100644
--- a/vernac/class.mli
+++ b/vernac/comCoercion.mli
@@ -9,7 +9,7 @@
(************************************************************************)
open Names
-open Classops
+open Coercionops
(** Classes and coercions. *)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 2aee9bd47f..8de1c69424 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -255,7 +255,7 @@ let inductive_levels env evd arities inds =
in
let cstrs_levels, min_levels, sizes =
CList.split3
- (List.map2 (fun (_,tys,_) (arity,(ctx,du)) ->
+ (List.map2 (fun (_,tys) (arity,(ctx,du)) ->
let len = List.length tys in
let minlev = Sorts.univ_of_sort du in
let minlev =
@@ -323,18 +323,18 @@ let check_named {CAst.loc;v=na} = match na with
let msg = str "Parameters must be named." in
user_err ?loc msg
-let template_polymorphism_candidate env ~ctor_levels uctx params concl =
+let template_polymorphism_candidate ~template_check ~ctor_levels uctx params concl =
match uctx with
| Entries.Monomorphic_entry uctx ->
let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in
if not concltemplate then false
+ else if not template_check then true
else
- let template_check = Environ.check_template env in
let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in
let params, conclunivs =
IndTyping.template_polymorphic_univs ~template_check ~ctor_levels uctx params conclu
in
- not (template_check && Univ.LSet.is_empty conclunivs)
+ not (Univ.LSet.is_empty conclunivs)
| Entries.Polymorphic_entry _ -> false
let check_param = function
@@ -350,33 +350,28 @@ let restrict_inductive_universes sigma ctx_params arities constructors =
let uvars = Univ.LSet.empty in
let uvars = Context.Rel.(fold_outside (Declaration.fold_constr merge_universes_of_constr) ctx_params ~init:uvars) in
let uvars = List.fold_right merge_universes_of_constr arities uvars in
- let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
+ let uvars = List.fold_right (fun (_,ctypes) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
Evd.restrict_universe_context sigma uvars
-let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_params ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
+let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
(* Compute renewed arities *)
let sigma = Evd.minimize_universes sigma in
let nf = Evarutil.nf_evars_universes sigma in
- let constructors = List.map (on_pi2 (List.map nf)) constructors in
+ let constructors = List.map (on_snd (List.map nf)) constructors in
let arities = List.map EConstr.(to_constr sigma) arities in
let sigma = List.fold_left make_anonymous_conclusion_flexible sigma arityconcl in
let sigma, arities = inductive_levels env_ar_params sigma arities constructors in
let sigma = Evd.minimize_universes sigma in
let nf = Evarutil.nf_evars_universes sigma in
let arities = List.map (on_snd nf) arities in
- let constructors = List.map (on_pi2 (List.map nf)) constructors in
+ let constructors = List.map (on_snd (List.map nf)) constructors in
let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
let arityconcl = List.map (Option.map (fun (_anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in
let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in
let uctx = Evd.check_univ_decl ~poly sigma udecl in
- List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr (snd c))) arities;
- Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params;
- List.iter (fun (_,ctyps,_) ->
- List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps)
- constructors;
(* Build the inductive entries *)
- let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes,cimpls) ->
+ let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes) ->
let template_candidate () =
templatearity ||
let ctor_levels =
@@ -390,7 +385,7 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa
List.fold_left (fun levels c -> add_levels c levels)
param_levels ctypes
in
- template_polymorphism_candidate env0 ~ctor_levels uctx ctx_params concl
+ template_polymorphism_candidate ~template_check:(Environ.check_template env_ar_params) ~ctor_levels uctx ctx_params concl
in
let template = match template with
| Some template ->
@@ -408,7 +403,6 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa
})
indnames arities arityconcl constructors
in
- let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance uctx) else None in
(* Build the mutual inductive entry *)
let mind_ent =
{ mind_entry_params = ctx_params;
@@ -417,12 +411,10 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa
mind_entry_inds = entries;
mind_entry_private = if private_ind then Some false else None;
mind_entry_universes = uctx;
- mind_entry_variance = variance;
+ mind_entry_cumulative = poly && cumulative;
}
in
- (if poly && cumulative then
- InferCumulativity.infer_inductive env_ar mind_ent
- else mind_ent), Evd.universe_binders sigma
+ mind_ent, Evd.universe_binders sigma
let interp_params env udecl uparamsl paramsl =
let sigma, udecl = interp_univ_decl_opt env udecl in
@@ -492,9 +484,10 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
List.init (List.length indl) EConstr.(fun i -> mkApp (mkRel (i + 1 + nuparams), uargs))
@ List.init nuparams EConstr.(fun i -> mkRel (i + 1)) in
let generalize_constructor c = EConstr.Unsafe.to_constr (EConstr.Vars.substnl uparam_subst nparams c) in
+ let cimpls = List.map pi3 constructors in
let constructors = List.map (fun (cnames,ctypes,cimpls) ->
- (cnames,List.map generalize_constructor ctypes,cimpls))
- constructors
+ (cnames,List.map generalize_constructor ctypes))
+ constructors
in
let ctx_params = ctx_params @ ctx_uparams in
let userimpls = useruimpls @ userimpls in
@@ -505,11 +498,12 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
(* Try further to solve evars, and instantiate them *)
let sigma = solve_remaining_evars all_and_fail_flags env_params sigma in
let impls =
- List.map2 (fun indimpls (_,_,cimpls) ->
+ List.map2 (fun indimpls cimpls ->
indimpls, List.map (fun impls ->
- userimpls @ impls) cimpls) indimpls constructors
+ userimpls @ impls) cimpls)
+ indimpls cimpls
in
- let mie, pl = interp_mutual_inductive_constr ~env0 ~template ~sigma ~env_params ~env_ar ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in
+ let mie, pl = interp_mutual_inductive_constr ~template ~sigma ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in
(mie, pl, impls)
@@ -559,7 +553,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni
(* Declare the possible notations of inductive types *)
List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns;
(* Declare the coercions *)
- List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes
+ List.iter (fun qid -> ComCoercion.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes
(** Prepare a "match" template for a given inductive type.
For each branch of the match, we list the constructor name
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index ef05b213d8..cc104b3762 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -49,24 +49,22 @@ val declare_mutual_inductive_with_eliminations
-> Names.MutInd.t
[@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"]
-val interp_mutual_inductive_constr :
- env0:Environ.env ->
- sigma:Evd.evar_map ->
- template:bool option ->
- udecl:UState.universe_decl ->
- env_ar:Environ.env ->
- env_params:Environ.env ->
- ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list ->
- indnames:Names.Id.t list ->
- arities:EConstr.t list ->
- arityconcl:(bool * EConstr.ESorts.t) option list ->
- constructors:(Names.Id.t list * Constr.constr list * 'a list list) list ->
- env_ar_params:Environ.env ->
- cumulative:bool ->
- poly:bool ->
- private_ind:bool ->
- finite:Declarations.recursivity_kind ->
- Entries.mutual_inductive_entry * UnivNames.universe_binders
+val interp_mutual_inductive_constr
+ : sigma:Evd.evar_map
+ -> template:bool option
+ -> udecl:UState.universe_decl
+ -> ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list
+ -> indnames:Names.Id.t list
+ -> arities:EConstr.t list
+ -> arityconcl:(bool * EConstr.ESorts.t) option list
+ -> constructors:(Names.Id.t list * Constr.constr list) list
+ -> env_ar_params:Environ.env
+ (** Environment with the inductives and parameters in the rel_context *)
+ -> cumulative:bool
+ -> poly:bool
+ -> private_ind:bool
+ -> finite:Declarations.recursivity_kind
+ -> Entries.mutual_inductive_entry * UnivNames.universe_binders
(************************************************************************)
(** Internal API, exported for Record *)
@@ -78,17 +76,17 @@ val should_auto_template : Id.t -> bool -> bool
inductive under consideration. *)
val template_polymorphism_candidate
- : Environ.env
+ : template_check:bool
-> ctor_levels:Univ.LSet.t
-> Entries.universes_entry
-> Constr.rel_context
-> Sorts.t option
-> bool
-(** [template_polymorphism_candidate env ~ctor_levels uctx params
+(** [template_polymorphism_candidate ~template_check ~ctor_levels uctx params
conclsort] is [true] iff an inductive with params [params],
conclusion [conclsort] and universe levels appearing in the
constructor arguments [ctor_levels] would be definable as template
polymorphic. It should have at least one universe in its
monomorphic universe context that can be made parametric in its
- conclusion sort, if one is given. If the [Template Check] flag is
+ conclusion sort, if one is given. If the [template_check] flag is
false we just check that the conclusion sort is not small. *)
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 54dda09e83..c816a4eb4f 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -550,7 +550,7 @@ let intern_arg (acc, cst) (idl,(typ,ann)) =
let lib_dir = Lib.library_dp() in
let env = Global.env() in
let (mty, _, cst') = Modintern.interp_module_ast env Modintern.ModType typ in
- let () = Global.push_context_set true cst' in
+ let () = Global.push_context_set ~strict:true cst' in
let env = Global.env () in
let sobjs = get_module_sobjs false env inl mty in
let mp0 = get_module_path mty in
@@ -674,7 +674,7 @@ module RawModOps = struct
let start_module export id args res fs =
let mp = Global.start_module id in
let arg_entries_r, cst = intern_args args in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
let env = Global.env () in
let res_entry_o, subtyps, cst = match res with
| Enforce (res,ann) ->
@@ -689,7 +689,7 @@ let start_module export id args res fs =
let typs, cst = build_subtypes env mp arg_entries_r resl in
None, typs, cst
in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps };
let prefix = Lib.start_module export id mp fs in
Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModule prefix));
@@ -782,7 +782,7 @@ let declare_module id args res mexpr_o fs =
| None -> None
| _ -> inl_res
in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
let mp_env,resolver = Global.add_module id entry inl in
(* Name consistency check : kernel vs. library *)
@@ -804,10 +804,10 @@ module RawModTypeOps = struct
let start_modtype id args mtys fs =
let mp = Global.start_modtype id in
let arg_entries_r, cst = intern_args args in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
let env = Global.env () in
let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
openmodtype_info := sub_mty_l;
let prefix = Lib.start_modtype id mp fs in
Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModtype prefix));
@@ -835,19 +835,19 @@ let declare_modtype id args mtys (mty,ann) fs =
then we adds the module parameters to the global env. *)
let mp = Global.start_modtype id in
let arg_entries_r, cst = intern_args args in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
let params = mk_params_entry arg_entries_r in
let env = Global.env () in
let mte, _, cst = Modintern.interp_module_ast env Modintern.ModType mty in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
let env = Global.env () in
(* We check immediately that mte is well-formed *)
let _, _, _, cst = Mod_typing.translate_mse env None inl mte in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
let env = Global.env () in
let entry = params, mte in
let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
let env = Global.env () in
let sobjs = get_functor_sobjs false env inl entry in
let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in
@@ -903,7 +903,7 @@ let type_of_incl env is_mod = function
let declare_one_include (me_ast,annot) =
let env = Global.env() in
let me, kind, cst = Modintern.interp_module_ast env Modintern.ModAny me_ast in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
let env = Global.env () in
let is_mod = (kind == Modintern.Module) in
let cur_mp = Lib.current_mp () in
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index e02f94629c..07656f9715 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -247,7 +247,7 @@ type (_, _) entry =
| TTReference : ('self, qualid) entry
| TTBigint : ('self, string) entry
| TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
-| TTConstrList : prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry
+| TTConstrList : notation_entry * prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry
| TTPattern : int -> ('self, cases_pattern_expr) entry
| TTOpenBinderList : ('self, local_binder_expr list) entry
| TTClosedBinderList : string Tok.p list -> ('self, local_binder_expr list list) entry
@@ -278,6 +278,10 @@ let find_custom_entry s =
try (find_custom_entry constr_custom_entry sc, find_custom_entry pattern_custom_entry sp)
with Not_found -> user_err Pp.(str "Undeclared custom entry: " ++ str s ++ str ".")
+let exists_custom_entry s = match find_custom_entry s with
+| _ -> true
+| exception _ -> false
+
let locality_of_custom_entry s = String.Set.mem s !custom_entry_locality
(* This computes the name of the level where to add a new rule *)
@@ -347,12 +351,12 @@ let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_sym
let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with
| TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat
-| TTConstrList (typ', [], forpat) ->
- begin match symbol_of_target InConstrEntry typ' assoc from forpat with
+| TTConstrList (s, typ', [], forpat) ->
+ begin match symbol_of_target s typ' assoc from forpat with
| MayRecNo s -> MayRecNo (Alist1 s)
| MayRecMay s -> MayRecMay (Alist1 s) end
-| TTConstrList (typ', tkl, forpat) ->
- begin match symbol_of_target InConstrEntry typ' assoc from forpat with
+| TTConstrList (s, typ', tkl, forpat) ->
+ begin match symbol_of_target s typ' assoc from forpat with
| MayRecNo s -> MayRecNo (Alist1sep (s, make_sep_rules tkl))
| MayRecMay s -> MayRecMay (Alist1sep (s, make_sep_rules tkl)) end
| TTPattern p -> MayRecNo (Aentryl (Constr.pattern, string_of_int p))
@@ -369,7 +373,7 @@ let interp_entry forpat e = match e with
| ETProdBigint -> TTAny TTBigint
| ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat))
| ETProdPattern p -> TTAny (TTPattern p)
-| ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
+| ETProdConstrList (s, p, tkl) -> TTAny (TTConstrList (s, p, tkl, forpat))
| ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList
| ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
diff --git a/vernac/egramcoq.mli b/vernac/egramcoq.mli
index f879d51660..6768d24d5c 100644
--- a/vernac/egramcoq.mli
+++ b/vernac/egramcoq.mli
@@ -19,4 +19,7 @@ val extend_constr_grammar : Notation_gram.one_notation_grammar -> unit
(** Add a term notation rule to the parsing system. *)
val create_custom_entry : local:bool -> string -> unit
+
+val exists_custom_entry : string -> bool
+
val locality_of_custom_entry : string -> bool
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 436648c163..3302231fd1 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -471,7 +471,7 @@ GRAMMAR EXTEND Gram
[ [ attr = LIST0 quoted_attributes ;
bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ];
rf_notation = decl_notation -> {
- let rf_canonical = attr |> List.flatten |> parse canonical in
+ let rf_canonical = attr |> List.flatten |> parse canonical_field in
let rf_subclass, rf_decl = bd in
rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ]
;
@@ -1026,7 +1026,8 @@ GRAMMAR EXTEND Gram
| IDENT "Coercions" -> { PrintCoercions }
| IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
-> { PrintCoercionPaths (s,t) }
- | IDENT "Canonical"; IDENT "Projections" -> { PrintCanonicalConversions }
+ | IDENT "Canonical"; IDENT "Projections"; qids = LIST0 smart_global
+ -> { PrintCanonicalConversions qids }
| IDENT "Typing"; IDENT "Flags" -> { PrintTypingFlags }
| IDENT "Tables" -> { PrintTables }
| IDENT "Options" -> { PrintTables (* A Synonymous to Tables *) }
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 19ec0a3642..ba7ae5069b 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -297,6 +297,7 @@ let explain_unification_error env sigma p1 p2 = function
strbrk " with term " ++ pr_leconstr_env env sigma rhs ++
strbrk " that would depend on itself"]
| NotClean ((evk,args),env,c) ->
+ let env = make_all_name_different env sigma in
[str "cannot instantiate " ++ quote (pr_existential_key sigma evk)
++ strbrk " because " ++ pr_leconstr_env env sigma c ++
strbrk " is not in its scope" ++
@@ -605,7 +606,7 @@ let rec explain_evar_kind env sigma evk ty =
let explain_typeclass_resolution env sigma evi k =
match Typeclasses.class_of_constr env sigma evi.evar_concl with
| Some _ ->
- let env = Evd.evar_filtered_env evi in
+ let env = Evd.evar_filtered_env env evi in
fnl () ++ str "Could not find an instance for " ++
pr_leconstr_env env sigma evi.evar_concl ++
pr_trailing_ne_context_of env sigma
@@ -622,7 +623,7 @@ let explain_placeholder_kind env sigma c e =
let explain_unsolvable_implicit env sigma evk explain =
let evi = Evarutil.nf_evar_info sigma (Evd.find_undefined sigma evk) in
- let env = Evd.evar_filtered_env evi in
+ let env = Evd.evar_filtered_env env evi in
let type_of_hole = pr_leconstr_env env sigma evi.evar_concl in
let pe = pr_trailing_ne_context_of env sigma in
strbrk "Cannot infer " ++
diff --git a/vernac/library.ml b/vernac/library.ml
index 244424de6b..0f7e7d2aa0 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -430,6 +430,22 @@ let error_recursively_dependent_library dir =
(* Security weakness: file might have been changed on disk between
writing the content and computing the checksum... *)
+let save_library_base f sum lib univs tasks proofs =
+ let ch = raw_extern_library f in
+ try
+ System.marshal_out_segment f ch (sum : seg_sum);
+ System.marshal_out_segment f ch (lib : seg_lib);
+ System.marshal_out_segment f ch (univs : seg_univ option);
+ System.marshal_out_segment f ch (tasks : 'tasks option);
+ System.marshal_out_segment f ch (proofs : seg_proofs);
+ close_out ch
+ with reraise ->
+ let reraise = CErrors.push reraise in
+ close_out ch;
+ Feedback.msg_warning (str "Removed file " ++ str f);
+ Sys.remove f;
+ iraise reraise
+
type ('document,'counters) todo_proofs =
| ProofsTodoNone (* for .vo *)
| ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *)
@@ -454,18 +470,17 @@ let save_library_to todo_proofs ~output_native_objects dir f otab =
match todo_proofs with
| ProofsTodoNone -> None, None
| ProofsTodoSomeEmpty _except ->
- None,
- Some (Univ.ContextSet.empty,false)
+ None, Some (Univ.ContextSet.empty,false)
| ProofsTodoSome (_except, tasks, rcbackup) ->
- let tasks =
- List.map Stateid.(fun (r,b) ->
+ let tasks =
+ List.map Stateid.(fun (r,b) ->
try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b
with Not_found -> assert b; { r with uuid = -1 }, b)
tasks in
- Some (tasks,rcbackup),
- Some (Univ.ContextSet.empty,false)
- in
- let sd = {
+ Some (tasks,rcbackup),
+ Some (Univ.ContextSet.empty,false)
+ in
+ let sd = {
md_name = dir;
md_deps = Array.of_list (current_deps ());
} in
@@ -475,36 +490,15 @@ let save_library_to todo_proofs ~output_native_objects dir f otab =
} in
if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then
error_recursively_dependent_library dir;
- (* Open the vo file and write the magic number *)
- let f' = f in
- let ch = raw_extern_library f' in
- try
- (* Writing vo payload *)
- System.marshal_out_segment f' ch (sd : seg_sum);
- System.marshal_out_segment f' ch (md : seg_lib);
- System.marshal_out_segment f' ch (utab : seg_univ option);
- System.marshal_out_segment f' ch (tasks : 'tasks option);
- System.marshal_out_segment f' ch (opaque_table : seg_proofs);
- close_out ch;
- (* Writing native code files *)
- if output_native_objects then
- let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
- Nativelib.compile_library dir ast fn
- with reraise ->
- let reraise = CErrors.push reraise in
- let () = Feedback.msg_warning (str "Removed file " ++ str f') in
- let () = close_out ch in
- let () = Sys.remove f' in
- iraise reraise
+ (* Writing vo payload *)
+ save_library_base f sd md utab tasks opaque_table;
+ (* Writing native code files *)
+ if output_native_objects then
+ let fn = Filename.dirname f ^"/"^ Nativecode.mod_uid_of_dirpath dir in
+ Nativelib.compile_library dir ast fn
let save_library_raw f sum lib univs proofs =
- let ch = raw_extern_library f in
- System.marshal_out_segment f ch (sum : seg_sum);
- System.marshal_out_segment f ch (lib : seg_lib);
- System.marshal_out_segment f ch (Some univs : seg_univ option);
- System.marshal_out_segment f ch (None : 'tasks option);
- System.marshal_out_segment f ch (proofs : seg_proofs);
- close_out ch
+ save_library_base f sum lib (Some univs) None proofs
module StringOrd = struct type t = string let compare = String.compare end
module StringSet = Set.Make(StringOrd)
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index e23522da9e..222e9eb825 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -611,7 +611,7 @@ let expand_list_rule s typ tkl x n p ll =
else if Int.equal i (p+n) then
let hds =
GramConstrListMark (p+n,true,p) :: hds
- @ [GramConstrNonTerminal (ETProdConstrList (typ,tkl), Some x)] in
+ @ [GramConstrNonTerminal (ETProdConstrList (s, typ,tkl), Some x)] in
distribute hds ll
else
distribute (GramConstrListMark (i+1,false,p) :: hds @ [main]) ll @
@@ -1654,10 +1654,16 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing
(**********************************************************************)
(* Declaration of custom entry *)
+let warn_custom_entry =
+ CWarnings.create ~name:"custom-entry-overriden" ~category:"parsing"
+ (fun s ->
+ strbrk "Custom entry " ++ str s ++ strbrk " has been overriden.")
+
let load_custom_entry _ _ = ()
let open_custom_entry _ (_,(local,s)) =
- Egramcoq.create_custom_entry ~local s
+ if Egramcoq.exists_custom_entry s then warn_custom_entry s
+ else Egramcoq.create_custom_entry ~local s
let cache_custom_entry o =
load_custom_entry 1 o;
@@ -1677,4 +1683,7 @@ let inCustomEntry : locality_flag * string -> obj =
classify_function = classify_custom_entry}
let declare_custom_entry local s =
- Lib.add_anonymous_leaf (inCustomEntry (local,s))
+ if Egramcoq.exists_custom_entry s then
+ user_err Pp.(str "Custom entry " ++ str s ++ str " already exists")
+ else
+ Lib.add_anonymous_leaf (inCustomEntry (local,s))
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 1742027076..a1bd99c237 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -513,8 +513,8 @@ let string_of_theorem_kind = let open Decls in function
keyword "Print Coercion Paths" ++ spc()
++ pr_class_rawexpr s ++ spc()
++ pr_class_rawexpr t
- | PrintCanonicalConversions ->
- keyword "Print Canonical Structures"
+ | PrintCanonicalConversions qids ->
+ keyword "Print Canonical Structures" ++ prlist pr_smart_global qids
| PrintTypingFlags ->
keyword "Print Typing Flags"
| PrintTables ->
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index eb7b28f15b..b999ce9f3f 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -199,7 +199,7 @@ let print_opacity ref =
(*******************)
let print_if_is_coercion ref =
- if Classops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else []
+ if Coercionops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else []
(*******************)
(* *)
@@ -951,7 +951,7 @@ let inspect env sigma depth =
(*************************************************************************)
(* Pretty-printing functions coming from classops.ml *)
-open Classops
+open Coercionops
let print_coercion_value v = Printer.pr_global v.coe_value
@@ -965,7 +965,7 @@ let print_path ((i,j),p) =
str"] : ") ++
print_class i ++ str" >-> " ++ print_class j
-let _ = Classops.install_path_printer print_path
+let _ = Coercionops.install_path_printer print_path
let print_graph () =
prlist_with_sep fnl print_path (inheritance_graph())
@@ -996,12 +996,24 @@ let print_path_between cls clt =
in
print_path ((i,j),p)
-let print_canonical_projections env sigma =
+let print_canonical_projections env sigma grefs =
+ let match_proj_gref ((x,y),c) gr =
+ GlobRef.equal x gr ||
+ begin match y with
+ | Const_cs y -> GlobRef.equal y gr
+ | _ -> false
+ end ||
+ GlobRef.equal c.o_ORIGIN gr
+ in
+ let projs =
+ List.filter (fun p -> List.for_all (match_proj_gref p) grefs)
+ (canonical_projections ())
+ in
prlist_with_sep fnl
(fun ((r1,r2),o) -> pr_cs_pattern r2 ++
str " <- " ++
pr_global r1 ++ str " ( " ++ pr_lconstr_env env sigma o.o_DEF ++ str " )")
- (canonical_projections ())
+ projs
(*************************************************************************)
diff --git a/vernac/prettyp.mli b/vernac/prettyp.mli
index dc4280f286..ac41f30c5d 100644
--- a/vernac/prettyp.mli
+++ b/vernac/prettyp.mli
@@ -52,8 +52,8 @@ val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t
val print_graph : unit -> Pp.t
val print_classes : unit -> Pp.t
val print_coercions : unit -> Pp.t
-val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t
-val print_canonical_projections : env -> Evd.evar_map -> Pp.t
+val print_path_between : Coercionops.cl_typ -> Coercionops.cl_typ -> Pp.t
+val print_canonical_projections : env -> Evd.evar_map -> GlobRef.t list -> Pp.t
(** Pretty-printing functions for type classes and instances *)
val print_typeclasses : unit -> Pp.t
diff --git a/vernac/record.ml b/vernac/record.ml
index d85b71df44..df9b4a0914 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -202,7 +202,7 @@ let typecheck_params_and_fields finite def poly pl ps records =
in
let univs = Evd.check_univ_decl ~poly sigma decl in
let ubinders = Evd.universe_binders sigma in
- let ce t = Pretyping.check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr t) in
+ let ce t = Pretyping.check_evars env0 sigma (EConstr.of_constr t) in
let () = List.iter (iter_constr ce) (List.rev newps) in
ubinders, univs, template, newps, imps, ans
@@ -366,8 +366,8 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
let refi = GlobRef.ConstRef kn in
Impargs.maybe_declare_manual_implicits false refi impls;
if flags.pf_subclass then begin
- let cl = Class.class_of_global (GlobRef.IndRef indsp) in
- Class.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
+ let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in
+ ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
end;
let i = if is_local_assum decl then i+1 else i in
(Some kn::sp_projs, i, Projection term::subst)
@@ -411,7 +411,6 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
| Polymorphic_entry (nas, ctx) ->
true, Polymorphic_entry (nas, ctx)
in
- let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance ctx) else None in
let binder_name =
match name with
| None ->
@@ -447,7 +446,8 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
univs)
param_levels fields
in
- ComInductive.template_polymorphism_candidate (Global.env ()) ~ctor_levels univs params
+ let template_check = Environ.check_template (Global.env ()) in
+ ComInductive.template_polymorphism_candidate ~template_check ~ctor_levels univs params
(Some (Sorts.sort_of_univ min_univ))
in
match template with
@@ -477,10 +477,9 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
mind_entry_inds = blocks;
mind_entry_private = None;
mind_entry_universes = univs;
- mind_entry_variance = variance;
+ mind_entry_cumulative = poly && cumulative;
}
in
- let mie = InferCumulativity.infer_inductive (Global.env ()) mie in
let impls = List.map (fun _ -> paramimpls, []) record_data in
let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls
~primitive_expected:!primitive_flag
@@ -490,7 +489,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
let cstr = (rsp, 1) in
let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
let build = GlobRef.ConstructRef cstr in
- let () = if is_coe then Class.try_add_new_coercion build ~local:false ~poly in
+ let () = if is_coe then ComCoercion.try_add_new_coercion build ~local:false ~poly in
let () = declare_structure_entry (cstr, List.rev kinds, List.rev sp_projs) in
rsp
in
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 5226c2ba65..7b4924eaed 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -21,7 +21,7 @@ RecLemmas
Library
Prettyp
Lemmas
-Class
+ComCoercion
Auto_ind_decl
Search
Indschemes
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e4965614d8..e98820bc98 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -49,9 +49,9 @@ let get_goal_or_global_context ~pstate glnum =
| Some p -> Pfedit.get_goal_context p glnum
let cl_of_qualid = function
- | FunClass -> Classops.CL_FUN
- | SortClass -> Classops.CL_SORT
- | RefClass r -> Class.class_of_global (Smartlocate.smart_global ~head:true r)
+ | FunClass -> Coercionops.CL_FUN
+ | SortClass -> Coercionops.CL_SORT
+ | RefClass r -> ComCoercion.class_of_global (Smartlocate.smart_global ~head:true r)
let scope_class_of_qualid qid =
Notation.scope_class_of_class (cl_of_qualid qid)
@@ -63,14 +63,15 @@ module DefAttributes = struct
polymorphic : bool;
program : bool;
deprecated : Deprecation.t option;
+ canonical_instance : bool;
}
let parse f =
let open Attributes in
- let ((locality, deprecated), polymorphic), program =
- parse Notations.(locality ++ deprecation ++ polymorphic ++ program) f
+ let (((locality, deprecated), polymorphic), program), canonical_instance =
+ parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance) f
in
- { polymorphic; program; locality; deprecated }
+ { polymorphic; program; locality; deprecated; canonical_instance }
end
let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l))
@@ -474,7 +475,7 @@ let program_inference_hook env sigma ev =
let tac = !Obligations.default_tactic in
let evi = Evd.find sigma ev in
let evi = Evarutil.nf_evar_info sigma evi in
- let env = Evd.evar_filtered_env evi in
+ let env = Evd.evar_filtered_env env evi in
try
let concl = evi.Evd.evar_concl in
if not (Evarutil.is_ground_env sigma env &&
@@ -522,13 +523,17 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
in
start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl
-let vernac_definition_hook ~local ~poly = let open Decls in function
+let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function
| Coercion ->
- Some (Class.add_coercion_hook ~poly)
+ Some (ComCoercion.add_coercion_hook ~poly)
| CanonicalStructure ->
Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
| SubClass ->
- Some (Class.add_subclass_hook ~poly)
+ Some (ComCoercion.add_subclass_hook ~poly)
+| Definition when canonical_instance ->
+ Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
+| Let when canonical_instance ->
+ Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref)))
| _ -> None
let fresh_name_for_anonymous_theorem () =
@@ -551,7 +556,7 @@ let vernac_definition_name lid local =
let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
let open DefAttributes in
let local = enforce_locality_exp atts.locality discharge in
- let hook = vernac_definition_hook ~local:atts.locality ~poly:atts.polymorphic kind in
+ let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in
let program_mode = atts.program in
let poly = atts.polymorphic in
let name = vernac_definition_name lid local in
@@ -560,7 +565,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt =
let open DefAttributes in
let scope = enforce_locality_exp atts.locality discharge in
- let hook = vernac_definition_hook ~local:atts.locality ~poly:atts.polymorphic kind in
+ let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in
let program_mode = atts.program in
let name = vernac_definition_name lid scope in
let red_option = match red_option with
@@ -1034,7 +1039,7 @@ let vernac_coercion ~atts ref qids qidt =
let target = cl_of_qualid qidt in
let source = cl_of_qualid qids in
let ref' = smart_global ref in
- Class.try_add_new_coercion_with_target ref' ~local ~poly ~source ~target;
+ ComCoercion.try_add_new_coercion_with_target ref' ~local ~poly ~source ~target;
Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
let vernac_identity_coercion ~atts id qids qidt =
@@ -1042,7 +1047,7 @@ let vernac_identity_coercion ~atts id qids qidt =
let local = enforce_locality local in
let target = cl_of_qualid qidt in
let source = cl_of_qualid qids in
- Class.try_add_new_identity_coercion id ~local ~poly ~source ~target
+ ComCoercion.try_add_new_identity_coercion id ~local ~poly ~source ~target
(* Type classes *)
@@ -1621,7 +1626,7 @@ let vernac_global_check c =
let c,uctx = interp_constr env sigma c in
let senv = Global.safe_env() in
let uctx = UState.context_set uctx in
- let senv = Safe_typing.push_context_set false uctx senv in
+ let senv = Safe_typing.push_context_set ~strict:false uctx senv in
let c = EConstr.to_constr sigma c in
let j = Safe_typing.typing senv c in
let env = Safe_typing.env_of_safe_env senv in
@@ -1701,7 +1706,9 @@ let vernac_print ~pstate ~atts =
| PrintCoercions -> Prettyp.print_coercions ()
| PrintCoercionPaths (cls,clt) ->
Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)
- | PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma
+ | PrintCanonicalConversions qids ->
+ let grefs = List.map Smartlocate.smart_global qids in
+ Prettyp.print_canonical_projections env sigma grefs
| PrintUniverses (sort, subgraph, dst) -> print_universes ~sort ~subgraph dst
| PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r)
| PrintHintGoal ->
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 32ff8b8fb2..1daa244986 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -46,7 +46,7 @@ type printable =
| PrintInstances of qualid or_by_notation
| PrintCoercions
| PrintCoercionPaths of class_rawexpr * class_rawexpr
- | PrintCanonicalConversions
+ | PrintCanonicalConversions of qualid or_by_notation list
| PrintUniverses of bool * qualid list option * string option
| PrintHint of qualid or_by_notation
| PrintHintGoal
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 22:36:23 +0000