diff options
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index c52f96079..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 @@ -974,9 +981,6 @@ let count_occurrences sigma m t = countrec m t; !n -(* Synonymous *) -let occur_term = dependent - let pop t = EConstr.Vars.lift (-1) t (***************************) |