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

(when we compare universes and implict annotations)

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index fb99090e98b76df165c3cbd8244ee17fb70c1601..bff721a3e7b5a247e9bca1e0f442b9202ee31a53 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/components/acic_procedural/acic2Procedural.ml
@@ -26,6 +26,7 @@
 module C    = Cic
 module I    = CicInspect
 module D    = Deannotate
+module S    = CicSubstitution
 module TC   = CicTypeChecker 
 module Un   = CicUniv
 module UM   = UriManager
@@ -183,17 +184,20 @@ let convert st ?name v =
    match get_inner_types st v with
       | None            -> []
       | Some (sty, ety) ->
+        let e = Cn.mk_pattern 0 (T.mk_arel 1 "") in
          let csty, cety = cic sty, cic ety in
         if Ut.alpha_equivalence csty cety then [] else 
-        let e = Cn.mk_pattern 0 (T.mk_arel 1 "") in
         match name with
-           | None    -> [T.Change (sty, ety, None, e, "")]
-           | Some id -> 
+           | None         -> [T.Change (sty, ety, None, e, "")]
+           | Some (id, i) -> 
                begin match get_entry st id with
                  | C.Def _  -> [T.ClearBody (id, "")]
                  | C.Decl w -> 
-                    if Ut.alpha_equivalence csty w then [] 
-                    else [T.Change (sty, ety, Some (id, id), e, "")] 
+                    let w = S.lift i w in
+                    if Ut.alpha_equivalence csty w then [] 
+                    else 
+                    [T.Note (Pp.ppterm csty); T.Note (Pp.ppterm w);
+                    T.Change (sty, ety, Some (id, id), e, "")] 
               end
 
 let get_intro = function 
@@ -206,7 +210,7 @@ let mk_intros st script =
    T.Intros (Some count, List.rev st.intros, "") :: script
 
 let mk_arg st = function
-   | C.ARel (_, _, _, name) as what -> convert st ~name what
+   | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what
    | _                              -> []
 
 let mk_fwd_rewrite st dtext name tl direction =   

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