diff options
| author | Enrico Tassi | 2020-02-13 17:24:57 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-02-13 17:24:57 +0100 |
| commit | 6e020b001ec8b9d84293c5e9e7115bb1ddf901ca (patch) | |
| tree | 987e80de2abda3cb2b898e05d39db07d320c5edb /engine/eConstr.mli | |
| parent | eb83c142eb33de18e3bfdd7c32ecfb797a640c38 (diff) | |
| parent | b468bb9e7110be4e1a1c9b13da16720b64d1125e (diff) | |
Merge PR #11417: Move kind_of_type from the kernel to EConstr.
Reviewed-by: SkySkimmer
Reviewed-by: gares
Diffstat (limited to 'engine/eConstr.mli')
| -rw-r--r-- | engine/eConstr.mli | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 181714460d..ead7d88176 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -80,7 +80,14 @@ val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t val to_constr_opt : Evd.evar_map -> t -> Constr.t option (** Same as [to_constr], but returns [None] if some unresolved evars remain *) -val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type +type kind_of_type = + | SortType of ESorts.t + | CastType of types * t + | ProdType of Name.t Context.binder_annot * t * t + | LetInType of Name.t Context.binder_annot * t * t * t + | AtomicType of t * t array + +val kind_of_type : Evd.evar_map -> t -> kind_of_type (** {5 Constructors} *) |