diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-04 18:58:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 23:05:31 +0100 |
| commit | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (patch) | |
| tree | fceac407f6e4254e107817b6140257bcc8f9755a /kernel/constr.mli | |
| parent | 0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff) | |
[api] Deprecate all legacy uses of Names in core.
This will allow to merge back `Names` with `API.Names`
Diffstat (limited to 'kernel/constr.mli')
| -rw-r--r-- | kernel/constr.mli | 12 |
1 files changed, 6 insertions, 6 deletions
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 *) |