From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 19 Jun 2006 12:58:20 +0000 (+0000)
Subject: occur_check and unification fixed. now Meta(i,[]) and Meta(i,[...]) are
X-Git-Tag: make_still_working~7165
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b9d067ff0d66913b7ade9fadc79064dedb4aa86f;p=helm.git

occur_check and unification fixed. now Meta(i,[]) and Meta(i,[...]) are
considered the same.
---

diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml
index e2f85fa2b..1c3daffec 100644
--- a/helm/software/components/tactics/paramodulation/inference.ml
+++ b/helm/software/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) ->