From f3abbc55ef160d1a65d4467bfe9b25b30b965a46 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 4 Nov 2017 18:58:27 +0100 Subject: [api] Deprecate all legacy uses of Names in core. This will allow to merge back `Names` with `API.Names` --- kernel/constr.mli | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'kernel/constr.mli') diff --git a/kernel/constr.mli b/kernel/constr.mli index 76dbf5530..da074d85c 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -15,7 +15,7 @@ open Names type 'a puniverses = 'a Univ.puniverses (** {6 Simply type aliases } *) -type pconstant = constant puniverses +type pconstant = Constant.t puniverses type pinductive = inductive puniverses type pconstructor = constructor puniverses @@ -113,8 +113,8 @@ val mkApp : constr * constr array -> constr val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses -(** Constructs a constant *) -val mkConst : constant -> constr +(** Constructs a Constant.t *) +val mkConst : Constant.t -> constr val mkConstU : pconstant -> constr (** Constructs a projection application *) @@ -208,7 +208,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = - [F] itself is not {!App} - and [[|P1;..;Pn|]] is not empty. *) - | Const of (constant * 'univs) (** Gallina-variable that was introduced by Vernacular-command that extends the global environment + | Const of (Constant.t * 'univs) (** Gallina-variable that was introduced by Vernacular-command that extends the global environment (i.e. [Parameter], or [Axiom], or [Definition], or [Theorem] etc.) *) | Ind of (inductive * 'univs) (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) @@ -302,7 +302,7 @@ val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool (** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed, [u] to compare universe - instances (the first boolean tells if they belong to a constant), [s] to + instances (the first boolean tells if they belong to a Constant.t), [s] to compare sorts; Cast's, binders name and Cases annotations are not taken into account *) @@ -335,7 +335,7 @@ val compare_head_gen_with : (** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] for conversion, [fle] for cumulativity, [u] to compare universe - instances (the first boolean tells if they belong to a constant), + instances (the first boolean tells if they belong to a Constant.t), [s] to compare sorts for for subtyping; Cast's, binders name and Cases annotations are not taken into account *) -- cgit v1.2.3