diff options
| author | Pierre-Marie Pédrot | 2018-10-17 15:29:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-17 15:29:47 +0200 |
| commit | 15998894ff76b1fa9354085ea0bddae4f8f23ddf (patch) | |
| tree | 254cc3a53b6aa344f49a10cba32e14acf97d2905 /kernel/constr.mli | |
| parent | 063cf49f40511730c8c60c45332e92823ce4c78f (diff) | |
| parent | 6aa0aa37e19457a8c0c3ad36f7bbead058442344 (diff) | |
Merge PR #8694: Various cleanups of universe apis
Diffstat (limited to 'kernel/constr.mli')
| -rw-r--r-- | kernel/constr.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index 3c9cc96a0d..c012f04260 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -128,6 +128,9 @@ val mkConstruct : constructor -> constr val mkConstructU : pconstructor -> constr val mkConstructUi : pinductive * int -> constr +(** Make a constant, inductive, constructor or variable. *) +val mkRef : GlobRef.t Univ.puniverses -> constr + (** Constructs a destructor of inductive type. [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] @@ -340,6 +343,8 @@ val destFix : constr -> fixpoint val destCoFix : constr -> cofixpoint +val destRef : constr -> GlobRef.t Univ.puniverses + (** {6 Equality} *) (** [equal a b] is true if [a] equals [b] modulo alpha, casts, |