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 7c18674a865ac9eea2fc2df00b389ebd470ebb3e..236ee28401fe6d2fba33d8d545dc890748baed4c 100644 (file)
--- 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