better exception

[helm.git] / components / cic_acic / cic2acic.ml

diff --git a/components/cic_acic/cic2acic.ml b/components/cic_acic/cic2acic.ml
index 8540e0e6492fb4c15c3026e38f47c94b38e52202..a7d3cbc70e07ad609b9f714594cea80d1a468566 100644 (file)
--- 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