X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcoercGraph.ml;h=e54b3a847dde2d9489cf142baaa09f7b8b79cb11;hb=9b09890767aaa93e512324f8e7f13e2cdeebac88;hp=2fa2c4b0c5ca4ba216534de62d26cbebb9e02bcd;hpb=70211a10f741fe77945f5a720596df2b686f344d;p=helm.git

diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml
index 2fa2c4b0c..e54b3a847 100644
--- a/helm/software/components/cic_unification/coercGraph.ml
+++ b/helm/software/components/cic_unification/coercGraph.ml
@@ -259,7 +259,7 @@ let rec min acc = function
   | [] -> acc
 ;;
 
-let meets metasenv subst context left right =
+let meets metasenv subst context (grow_left,left) (grow_right,right) =
   let saturate metasenv uo =
     match uo with 
     | None -> metasenv, None
@@ -270,8 +270,10 @@ let meets metasenv subst context left right =
   in
   List.map 
     (fun (c,uo1,uo2) -> 
-      let metasenv, uo1 = saturate metasenv uo1 in
-      let metasenv, uo2 = saturate metasenv uo2 in
+      let metasenv, uo1 = 
+        if grow_left then saturate metasenv uo1 else metasenv, None in
+      let metasenv, uo2 = 
+        if grow_right then saturate metasenv uo2 else metasenv, None in
       c,metasenv, uo1, uo2)
     (min [] (intersect (grow left) (grow right)))
 ;;