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: 0.4.95@7852~1165
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=df8f668d1369432dbfb7c74a4c4789f3353fcb45;p=helm.git

eta_fix default to false
---

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