eta_fixing of the CurrentProof metasenv is wrong, since eta_fix does not have

the context parameter. Fixed by avoiding CurrentProof metasenv eta_fixing.

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index f45a92c1ab81c355c86128a99fc7d58737d0c3a3..495cb0405ddc55bcde5987b085132fdbe0df45db 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -414,8 +414,8 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
   let aconjecture_of_conjecture' = aconjecture_of_conjecture seed 
     ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types 
     ids_to_hypotheses hypotheses_seed in 
-   let eta_fix context t =
-    if eta_fix then E.eta_fix context t else t
+   let eta_fix metasenv t =
+    if eta_fix then E.eta_fix metasenv t else t
    in
    let aobj =
     match obj with
@@ -445,6 +445,12 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
          ("mettereaposto",id,abo,aty, params)
     | C.CurrentProof (id,conjectures,bo,ty,params) ->
        let conjectures' =
+        (*CSC: This code is bugged, since it does a List.map instead
+         * of a List.fold, withouth calling eta_fixing with the
+         * current context. Indeed, eta_fix always starts now in the
+         * empty context. Instead of fixing this piece of code and
+         * adding a new argument to eta_fix, I just skip eta_fixing
+         * of the CurrentProof metasenv. Does this break well-typedness?
         List.map
          (function (i,canonical_context,term) ->
            let canonical_context' =
@@ -459,7 +465,8 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
            in
            let term' = eta_fix conjectures term in
             (i,canonical_context',term')
-         ) conjectures
+         ) conjectures *)
+         conjectures
        in
        let aconjectures = 
         List.map