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 fd2819738af77561725d77067926a694b90b9480..4dfe783012ed0fffe914037d30f8048c465b0f26 100644 (file)
--- 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