alpha equivalence fixed: in the case "meta against meta" we did not recur on theexpli...

[helm.git] / components / cic / cicUtil.ml

diff --git a/components/cic/cicUtil.ml b/components/cic/cicUtil.ml
index d79c233dfa100ad96a61a37e4ee8788190332563..22dcb298cdb929160f3b8f14e5ba5d3bbf36359c 100644 (file)
--- a/components/cic/cicUtil.ml
+++ b/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