From fe99a52453c40c840cfaa718e9e2646eaab87763 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 6 Apr 2004 12:38:20 +0000 Subject: [PATCH] eta_fixing of the CurrentProof metasenv is wrong, since eta_fix does not have the context parameter. Fixed by avoiding CurrentProof metasenv eta_fixing. --- helm/ocaml/cic_omdoc/cic2acic.ml | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index f45a92c1a..495cb0405 100644 --- 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 -- 2.39.2