X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=components%2Fcic_acic%2Fcic2acic.ml;h=a7d3cbc70e07ad609b9f714594cea80d1a468566;hb=3077a8a3657bba79d3edad3fb483122ea3126b72;hp=8540e0e6492fb4c15c3026e38f47c94b38e52202;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/cic_acic/cic2acic.ml b/components/cic_acic/cic2acic.ml
index 8540e0e64..a7d3cbc70 100644
--- a/components/cic_acic/cic2acic.ml
+++ b/components/cic_acic/cic2acic.ml
@@ -166,9 +166,9 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
           { D.synthesized =
 (***CSC: patch per provare i tempi
             CicReduction.whd context (xxx_type_of_aux' metasenv context tt) ; *)
-            if global_computeinnertypes then
+            (*if global_computeinnertypes then
               Cic.Sort (Cic.Type (CicUniv.fresh()))
-            else
+            else*)
               CicReduction.whd context (xxx_type_of_aux' metasenv context tt);
           D.expected = None}
         in