From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 21 Jul 2006 14:17:20 +0000 (+0000)
Subject: eta_fix default to false
X-Git-Tag: make_still_working~7025
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=984afddae60275147eac32185e546a7eb943bb6c;p=helm.git

eta_fix default to false
---

diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index 72837dab0..6da648453 100644
--- 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