From: Enrico Tassi Date: Thu, 29 May 2008 16:27:26 +0000 (+0000) Subject: CProp, since it was defined in CoRN as a Type, is predicative. X-Git-Tag: make_still_working~5105 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2b10614120e86ec755f4826c6e78a654434bc7f8;p=helm.git CProp, since it was defined in CoRN as a Type, is predicative. However, it is not Type0, but a moving Type as usual, for example inductive and (A,B:CProp) : CProp := ... inductive exists (A:Type) (P:A->CProp) : CProp := | ext : \forall x:A. \forall p : P x. exists A P. does not pass since the sort of x is Type not included in CProp. Putting exists in Type does not work either, if you want to make a conjuction involving an existential. solution, to be implemented: CProp of CicUniv.universe where CProp n is meant to be Type (n + 0.5). --- diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index fd2819738..4dfe78301 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -1834,10 +1834,10 @@ end; let t1' = CicReduction.whd ~subst context t1 in let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in match (t1', t2') with - (C.Sort s1, C.Sort s2) - when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> + | (C.Sort s1, C.Sort (C.Prop | C.Set)) -> (* different from Coq manual!!! *) - C.Sort s2,ugraph + t2',ugraph + | (C.Sort (C.Prop | C.Set | C.CProp), C.Sort C.CProp ) -> t2', ugraph | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *) let t' = CicUniv.fresh() in @@ -1847,7 +1847,8 @@ end; C.Sort (C.Type t'),ugraph2 with CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg)) - | (C.Sort _,C.Sort (C.Type t1)) -> + | (C.Sort _,C.Sort (C.Type t1)) + | (C.Sort (C.Type t1), C.Sort C.CProp) -> (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *) C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *) | (C.Meta _, C.Sort _) -> t2',ugraph