eta_fix default to false

diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index 72837dab0f954b3e264284a480d833357c13f186..6da6484535f53f3922ad0f735074727c02c32a3e 100644 (file)
--- a/helm/software/components/cic_acic/cic2acic.ml
+++ b/helm/software/components/cic_acic/cic2acic.ml
@@ -474,7 +474,7 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
       ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses))
 ;;
 
-let acic_object_of_cic_object ?(eta_fix=true) obj =
+let acic_object_of_cic_object ?(eta_fix=false) obj =
  let module C = Cic in
  let module E = Eta_fixing in
   let ids_to_terms = Hashtbl.create 503 in