diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 8 | ||||
| -rw-r--r-- | engine/eConstr.mli | 2 |
2 files changed, 10 insertions, 0 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 3385b78958..cfc4bea85f 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -99,6 +99,14 @@ let isFix sigma c = match kind sigma c with Fix _ -> true | _ -> false let isCoFix sigma c = match kind sigma c with CoFix _ -> true | _ -> false let isCase sigma c = match kind sigma c with Case _ -> true | _ -> false let isProj sigma c = match kind sigma c with Proj _ -> true | _ -> false + +let rec isType sigma c = match kind sigma c with + | Sort s -> (match ESorts.kind sigma s with + | Sorts.Type _ -> true + | _ -> false ) + | Cast (c,_,_) -> isType sigma c + | _ -> false + let isVarId sigma id c = match kind sigma c with Var id' -> Id.equal id id' | _ -> false let isRelN sigma n c = diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 1edc0ee12b..6532e08e9d 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -157,6 +157,8 @@ val isCoFix : Evd.evar_map -> t -> bool val isCase : Evd.evar_map -> t -> bool val isProj : Evd.evar_map -> t -> bool +val isType : Evd.evar_map -> constr -> bool + type arity = rel_context * ESorts.t val destArity : Evd.evar_map -> types -> arity val isArity : Evd.evar_map -> t -> bool |