From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 19 Jun 2002 10:44:15 +0000 (+0000)
Subject: Bug fixed: a sort not in normal form can now also be a LetIn.
X-Git-Tag: V_0_3_0_debian_8~30
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9be4bd4ab358f073626a6926271c2e3c5694f7a0;p=helm.git

Bug fixed: a sort not in normal form can now also be a LetIn.
---

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index 7c18674a8..236ee2840 100644
--- a/helm/gTopLevel/cic2acic.ml
+++ b/helm/gTopLevel/cic2acic.ml
@@ -70,8 +70,8 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
       (*CSC: This is a very inefficient way of computing inner types *)
       (*CSC: and inner sorts: very deep terms have their types/sorts *)
       (*CSC: computed again and again.                               *)
-      let string_of_sort =
-       function 
+      let string_of_sort t =
+       match CicReduction.whd context t with 
           C.Sort C.Prop -> "Prop"
         | C.Sort C.Set  -> "Set"
         | C.Sort C.Type -> "Type"
@@ -100,7 +100,6 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
                match expected with
                   None -> None,false
                 | Some expectedty' ->
-prerr_endline ("###: " ^ CicPp.ppterm synthesized ^ " <==> " ^ CicPp.ppterm expectedty') ; flush stderr ;
                    Some (aux false (Some fresh_id'') context expectedty'),true
             in
              Some