From 9be4bd4ab358f073626a6926271c2e3c5694f7a0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 19 Jun 2002 10:44:15 +0000 Subject: [PATCH] Bug fixed: a sort not in normal form can now also be a LetIn. --- helm/gTopLevel/cic2acic.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) 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 -- 2.39.2