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

[helm.git] / components / acic_procedural / acic2Procedural.ml

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 =