From e507075709b73f1e62e6f3f555675063087140ec Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 19 Jun 2006 12:58:20 +0000 Subject: [PATCH] occur_check and unification fixed. now Meta(i,[]) and Meta(i,[...]) are considered the same. --- components/tactics/paramodulation/inference.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml index e2f85fa2b..1c3daffec 100644 --- a/components/tactics/paramodulation/inference.ml +++ b/components/tactics/paramodulation/inference.ml @@ -70,7 +70,7 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = let lookup = Subst.lookup_subst in let rec occurs_check subst what where = match where with - | t when what = t -> true + | Cic.Meta(i,_) when i = what -> true | C.Appl l -> List.exists (occurs_check subst what) l | C.Meta _ -> let t = lookup where subst in @@ -84,6 +84,9 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = in match s, t with | s, t when s = t -> subst, menv + (* sometimes the same meta has different local contexts; this + could create "cyclic" substitutions *) + | C.Meta (i, _), C.Meta (j, _) when i=j -> subst, menv | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) &&(locked locked_menv j) -> raise @@ -92,7 +95,7 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = unif subst menv t s | C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) -> unif subst menv t s - | C.Meta _, t when occurs_check subst s t -> + | C.Meta (i,_), t when occurs_check subst i t -> raise (U.UnificationFailure (lazy "Inference.unification.unif")) | C.Meta (i, l), t when (locked locked_menv i) -> -- 2.39.2