From 7913b03ba5072efeb9f6ef009ce27cec8ff19cac Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 10 Apr 2018 18:24:45 +0200 Subject: Replace uses of Termops.dependent by more specific functions. This is more efficient in general, because Termops.dependent doesn't take advantage of the knowledge of its pattern argument. --- engine/termops.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'engine/termops.ml') diff --git a/engine/termops.ml b/engine/termops.ml index b7531f6fc..e9d17e3c5 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -851,6 +851,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 -- cgit v1.2.3