diff options
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index aa6cc297b..99252ce65 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -473,6 +473,13 @@ let occur_existential c = | _ -> iter_constr occrec c in try occrec c; false with Occur -> true +let occur_meta_or_existential c = + let rec occrec c = match kind_of_term c with + | Evar _ -> raise Occur + | Meta _ -> raise Occur + | _ -> iter_constr occrec c + in try occrec c; false with Occur -> true + let occur_const s c = let rec occur_rec c = match kind_of_term c with | Const sp when sp=s -> raise Occur |