aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/termops.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2018-06-04 14:11:33 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2018-06-04 14:11:33 +0200
commit51555af3cccae1f73bfe97e4347a5c625c6d0ec6 (patch)
tree393ec356983e72158e52916cb06f8767f1a49587 /engine/termops.ml
parent1757f89b6c61024bbe3aebd6b43c56df0d92f5eb (diff)
parent7913b03ba5072efeb9f6ef009ce27cec8ff19cac (diff)
Merge PR #7216: Replace uses of Termops.dependent by more specific functions.
Diffstat (limited to 'engine/termops.ml')
-rw-r--r--engine/termops.ml7
1 files changed, 7 insertions, 0 deletions
diff --git a/engine/termops.ml b/engine/termops.ml
index 51fc59289..0c567754a 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -857,6 +857,13 @@ let occur_meta_or_existential sigma c =
| _ -> EConstr.iter sigma occrec c
in try occrec c; false with Occur -> true
+let occur_metavariable sigma m c =
+ let rec occrec c = match EConstr.kind sigma c with
+ | Meta m' -> if Int.equal m m' then raise Occur
+ | _ -> EConstr.iter sigma occrec c
+ in
+ try occrec c; false with Occur -> true
+
let occur_evar sigma n c =
let rec occur_rec c = match EConstr.kind sigma c with
| Evar (sp,_) when Evar.equal sp n -> raise Occur