diff options
Diffstat (limited to 'engine/eConstr.mli')
| -rw-r--r-- | engine/eConstr.mli | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 90f50b764c..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} *) @@ -152,6 +159,7 @@ val mkNamedProd_or_LetIn : named_declaration -> types -> types val isRel : Evd.evar_map -> t -> bool val isVar : Evd.evar_map -> t -> bool val isInd : Evd.evar_map -> t -> bool +val isRef : Evd.evar_map -> t -> bool val isEvar : Evd.evar_map -> t -> bool val isMeta : Evd.evar_map -> t -> bool val isSort : Evd.evar_map -> t -> bool @@ -175,6 +183,7 @@ val isArity : Evd.evar_map -> t -> bool val isVarId : Evd.evar_map -> Id.t -> t -> bool val isRelN : Evd.evar_map -> int -> t -> bool +val isRefX : Evd.evar_map -> GlobRef.t -> t -> bool val destRel : Evd.evar_map -> t -> int val destMeta : Evd.evar_map -> t -> metavariable @@ -319,6 +328,7 @@ val fresh_global : Evd.evar_map -> GlobRef.t -> Evd.evar_map * t val is_global : Evd.evar_map -> GlobRef.t -> t -> bool +[@@ocaml.deprecated "Use [EConstr.isRefX] instead."] (** {5 Extra} *) |