X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2acic.ml;h=37e56406e61db0b40b1d589287361a0323323e50;hb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;hp=bf686ac4e6e1781cf505d6e8330cf86dd3542cf9;hpb=4adceafdaa4cd82c427ac9de494179c242e7ad28;p=helm.git diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index bf686ac4e..37e56406e 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -108,7 +108,7 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts match CicReduction.whd context t with C.Sort C.Prop -> "Prop" | C.Sort C.Set -> "Set" - | C.Sort C.Type -> "Type" + | C.Sort (C.Type _) -> "Type" (* TASSI OK*) | C.Sort C.CProp -> "CProp" | C.Meta _ -> prerr_endline "Cic2acic: string_of_sort applied to a meta" ; @@ -134,7 +134,7 @@ prerr_endline "Cic2acic: string_of_sort applied to a meta" ; {D.synthesized = (***CSC: patch per provare i tempi CicReduction.whd context (xxx_type_of_aux' metasenv context tt) ; *) -Cic.Sort Cic.Type ; +Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *) D.expected = None} in incr number_new_type_of_aux' ; @@ -162,7 +162,8 @@ Cic.Sort Cic.Type ; with Not_found -> (* l'inner-type non e' nella tabella ==> sort <> Prop *) (* CSC: Type or Set? I can not tell *) - None,Cic.Sort Cic.Type,"Type",false + None,Cic.Sort (Cic.Type (CicUniv.fresh())),"Type",false + (* TASSI non dovrebbe fare danni *) (* *) in let add_inner_type id =