Cic2acic is now responsible of eta-fixing the objects (using the Eta_fix

[helm.git] / helm / ocaml / cic_omdoc / cic2acic.ml

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index a3cdfbb78603d3237e3006fc5ecfb41543a279e5..b8679dc62e0b32df9beea1added139d870af5a7b 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -298,6 +298,7 @@ let acic_of_cic_context metasenv context idrefs t =
 
 let acic_object_of_cic_object obj =
  let module C = Cic in
+ let module E = Eta_fixing in
   let ids_to_terms = Hashtbl.create 503 in
   let ids_to_father_ids = Hashtbl.create 503 in
   let ids_to_inner_sorts = Hashtbl.create 503 in
@@ -314,24 +315,45 @@ let acic_object_of_cic_object obj =
    let aobj =
     match obj with
       C.Constant (id,Some bo,ty,params) ->
-       let abo = acic_term_of_cic_term' bo (Some ty) in
-       let aty = acic_term_of_cic_term' ty None in
+       let bo' = E.eta_fix [] bo in
+       let ty' = E.eta_fix [] ty in
+       let abo = acic_term_of_cic_term' bo' (Some ty') in
+       let aty = acic_term_of_cic_term' ty' None in
         C.AConstant
-         ("mettereaposto",Some "mettereaposto2",id,Some abo,aty, params)
+         ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params)
     | C.Constant (id,None,ty,params) ->
-       let aty = acic_term_of_cic_term' ty None in
+       let ty' = E.eta_fix [] ty in
+       let aty = acic_term_of_cic_term' ty' None in
         C.AConstant
-         ("mettereaposto",None,id,None,aty, params)
+         ("mettereaposto",None,id,None,aty,params)
     | C.Variable (id,bo,ty,params) ->
+       let ty' = E.eta_fix [] ty in
        let abo =
         match bo with
            None -> None
-         | Some bo -> Some (acic_term_of_cic_term' bo (Some ty))
+         | Some bo ->
+            let bo' = E.eta_fix [] bo in
+             Some (acic_term_of_cic_term' bo' (Some ty'))
        in
-       let aty = acic_term_of_cic_term' ty None in
+       let aty = acic_term_of_cic_term' ty' None in
         C.AVariable
          ("mettereaposto",id,abo,aty, params)
     | C.CurrentProof (id,conjectures,bo,ty,params) ->
+       let conjectures' =
+        List.map
+         (function (i,canonical_context,term) ->
+           let canonical_context' =
+            List.map
+             (function
+                 None -> None
+               | Some (n, C.Decl t)-> Some (n, C.Decl (E.eta_fix conjectures t))
+               | Some (n, C.Def t) -> Some (n, C.Def (E.eta_fix conjectures t))
+             ) canonical_context
+           in
+           let term' = E.eta_fix conjectures term in
+            (i,canonical_context',term')
+         ) conjectures
+       in
        let aconjectures =
         List.map
          (function (i,canonical_context,term) as conjecture ->
@@ -377,10 +399,12 @@ let acic_object_of_cic_object obj =
                canonical_context idrefs' term None
              in
               (cid,i,(List.rev revacanonical_context),aterm)
-         ) conjectures in
+         ) conjectures' in
+       let bo' = E.eta_fix conjectures' bo in
+       let ty' = E.eta_fix conjectures' ty in
        let abo =
-        acic_term_of_cic_term_context' conjectures [] [] bo (Some ty) in
-       let aty = acic_term_of_cic_term_context' conjectures [] [] ty None in
+        acic_term_of_cic_term_context' conjectures' [] [] bo' (Some ty') in
+       let aty = acic_term_of_cic_term_context' conjectures' [] [] ty' None in
         C.ACurrentProof
          ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params)
     | C.InductiveDefinition (tys,params,paramsno) ->