diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-04 14:11:33 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-04 14:11:33 +0200 |
| commit | 51555af3cccae1f73bfe97e4347a5c625c6d0ec6 (patch) | |
| tree | 393ec356983e72158e52916cb06f8767f1a49587 /engine | |
| parent | 1757f89b6c61024bbe3aebd6b43c56df0d92f5eb (diff) | |
| parent | 7913b03ba5072efeb9f6ef009ce27cec8ff19cac (diff) | |
Merge PR #7216: Replace uses of Termops.dependent by more specific functions.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.ml | 7 | ||||
| -rw-r--r-- | engine/termops.mli | 1 |
2 files changed, 8 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 diff --git a/engine/termops.mli b/engine/termops.mli index bb3cbb6a8..6e63539ca 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -94,6 +94,7 @@ exception Occur val occur_meta : Evd.evar_map -> constr -> bool val occur_existential : Evd.evar_map -> constr -> bool val occur_meta_or_existential : Evd.evar_map -> constr -> bool +val occur_metavariable : Evd.evar_map -> metavariable -> constr -> bool val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool val occur_var_in_decl : |