X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUtil.ml;h=22dcb298cdb929160f3b8f14e5ba5d3bbf36359c;hb=834f5d5e341519cbb7c77b4fff5b0b3c7d425e6b;hp=d79c233dfa100ad96a61a37e4ee8788190332563;hpb=b4027b84fae91e907b6874060b91d89b6a1ad780;p=helm.git

diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml
index d79c233df..22dcb298c 100644
--- a/helm/software/components/cic/cicUtil.ml
+++ b/helm/software/components/cic/cicUtil.ml
@@ -526,7 +526,22 @@ let alpha_equivalence =
            ) true fl fl'
          with
           Invalid_argument _ -> false)
-     | _,_ -> false (* we already know that t != t' *)
+     | C.Meta (i, subst), C.Meta (i', subst') ->
+        i = i' &&
+        (try
+          List.fold_left2
+           (fun b xt xt' -> match xt,xt' with
+	     | Some t, Some t' -> b && aux t t'
+	     | _               -> b
+           ) true subst subst'
+         with
+          Invalid_argument _ -> false)     
+(* FG: are we _really_ sure of these?      
+     | C.Sort (C.Type u), C.Sort (C.Type u') -> u = u' 
+     | C.Implicit a, C.Implicit a' -> a = a'
+   we insert an unused variable below to genarate a warning at compile time
+*)     
+     | _,_ -> let fix_alpha_equivalence_please = 0 in false (* we already know that t != t' *)
   and aux_exp_named_subst exp_named_subst1 exp_named_subst2 =
    try
      List.fold_left2