From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 30 May 2008 19:28:41 +0000 (+0000)
Subject: CProp hierarchy is there!
X-Git-Tag: make_still_working~5094
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6719c0e318b312b51b089fea3d69d1b7103245ea;p=helm.git

CProp hierarchy is there!

Implications:
  - more universes, XML file format changed, please rebuild your stuff
  - CProp conclusions are eliminated with _rect and not _rec
  - CProp and Types are interleaved, but still comparable, this may (or not)
    what you expect: Type_i < CProp_i < Type_i+1 < CProp_i+1

Caveats:
  - are_convertible sort CProp may turn to be wrong, since Type_i is convertible    (<=) to CProp_i+0.5 and there is no way to set test_equality_only, an
    additional parameter may be useful
  - CProp goals will be tackled by auto even if they could be cumulated into
    Type that is not (by default) take into consideration
---

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 50312ff12..6ea839ce3 100644
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -158,7 +158,7 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Sort `Set -> "Set"
     | Ast.Sort `Prop -> "Prop"
     | Ast.Sort (`Type _) -> "Type"
-    | Ast.Sort `CProp -> "CProp"
+    | Ast.Sort (`CProp _)-> "CProp"
     | Ast.Symbol (name, _) -> "'" ^ name
 
     | Ast.UserInput -> ""
diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml
index d9d92ad6f..cc481ff0a 100644
--- a/helm/software/components/acic_content/cicNotationPt.ml
+++ b/helm/software/components/acic_content/cicNotationPt.ml
@@ -29,7 +29,7 @@
 
 type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
 type induction_kind = [ `Inductive | `CoInductive ]
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe]
 type fold_kind = [ `Left | `Right ]
 
 type location = Stdpp.location
diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml
index 2ce47bb67..7a4590849 100644
--- a/helm/software/components/acic_content/termAcicContent.ml
+++ b/helm/software/components/acic_content/termAcicContent.ml
@@ -103,14 +103,14 @@ let ast_of_acic0 ~output_type term_info acic k =
     | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
     | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set)
     | Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u))
-    | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
+    | Cic.ASort (id,Cic.CProp u) -> idref id (Ast.Sort (`CProp u))
     | Cic.AImplicit (id, Some `Hole) -> idref id Ast.UserInput
     | Cic.AImplicit (id, _) -> idref id Ast.Implicit
     | Cic.AProd (id,n,s,t) ->
         let binder_kind =
           match sort_of_id id with
           | `Set | `Type _ -> `Pi
-          | `Prop | `CProp -> `Forall
+          | `Prop | `CProp _ -> `Forall
         in
         idref id (Ast.Binder (binder_kind,
           (CicNotationUtil.name_of_cic_name n, Some (k s)), k t))
diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index d599bdeb2..4d8652107 100644
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -133,7 +133,7 @@ let get_default_eliminator context uri tyno ty =
    let ext = match get_tail context (get_type context ty) with
       | C.Sort C.Prop     -> "_ind"
       | C.Sort C.Set      -> "_rec"
-      | C.Sort C.CProp    -> "_rec"
+      | C.Sort (C.CProp _)   -> "_rect"
       | C.Sort (C.Type _) -> "_rect"
       | t                 -> 
          Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
diff --git a/helm/software/components/cic/cic.ml b/helm/software/components/cic/cic.ml
index 5dd8455ea..53b4ef62b 100644
--- a/helm/software/components/cic/cic.ml
+++ b/helm/software/components/cic/cic.ml
@@ -49,7 +49,7 @@ type sort =
    Prop
  | Set
  | Type of CicUniv.universe
- | CProp
+ | CProp of CicUniv.universe
 
 type name =
  | Name of string
diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml
index e61ee78ea..30e7a0b38 100644
--- a/helm/software/components/cic/cicParser.ml
+++ b/helm/software/components/cic/cicParser.ml
@@ -300,23 +300,26 @@ let impredicative_set = ref true;;
 
 let sort_of_string ctxt = function
   | "Prop" -> Cic.Prop
-  | "CProp" -> Cic.CProp
   (* THIS CASE IS HERE ONLY TO ALLOW THE PARSING OF COQ LIBRARY
    * THIS SHOULD BE REMOVED AS SOON AS univ_maker OR COQ'S EXPORTATION 
    * IS FIXED *)
+  | "CProp" -> Cic.CProp (CicUniv.fresh ~uri:ctxt.uri ())
   | "Type" ->  Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
   | "Set" when !impredicative_set -> Cic.Set
   | "Set" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
   | s ->
       let len = String.length s in
-      if not(len > 5) then parse_error ctxt "sort expected";
-      if not(String.sub s 0 5 = "Type:") then parse_error ctxt "sort expected";
-      let s = String.sub s 5 (len - 5) in
+      let sort_len, mk_sort = 
+        if len > 5 && String.sub s 0 5 = "Type:" then 5,fun x -> Cic.Type x 
+        else if len > 6 && String.sub s 0 6 = "CProp:" then 6,fun x->Cic.CProp x
+        else parse_error ctxt "sort expected"
+      in
+      let s = String.sub s sort_len (len - sort_len) in
       let i = String.index s ':' in  
       let id =  int_of_string (String.sub s 0 i) in
-      let suri = String.sub s (i+1) (len - 5 - i - 1) in
+      let suri = String.sub s (i+1) (len - sort_len - i - 1) in
       let uri = UriManager.uri_of_string suri in
-      try Cic.Type (CicUniv.fresh ~uri ~id ())
+      try mk_sort (CicUniv.fresh ~uri ~id ())
       with
       | Failure "int_of_string" 
       | Invalid_argument _ -> parse_error ctxt "sort expected" 
diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index b039b7e5b..01a4bb144 100644
--- a/helm/software/components/cic_acic/cic2acic.ml
+++ b/helm/software/components/cic_acic/cic2acic.ml
@@ -25,19 +25,20 @@
 
 (* $Id$ *)
 
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe  ]
 
 let string_of_sort = function
   | `Prop -> "Prop"
   | `Set -> "Set"
   | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)
-  | `CProp -> "CProp"
+  | `CProp u -> "CProp:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)
+
 
 let sort_of_sort = function
   | Cic.Prop  -> `Prop
   | Cic.Set   -> `Set
   | Cic.Type u -> `Type u
-  | Cic.CProp -> `CProp
+  | Cic.CProp u -> `CProp u
 
 (* let hashtbl_add_time = ref 0.0;; *)
 
@@ -149,7 +150,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
         | C.Sort C.Set   -> `Set
         | C.Sort (C.Type u) -> `Type u
         | C.Meta _       -> `Type (CicUniv.fresh())
-        | C.Sort C.CProp -> `CProp
+        | C.Sort (C.CProp u) -> `CProp u
         | t              ->
             prerr_endline ("Cic2acic.sort_of applied to: " ^ CicPp.ppterm t) ;
             assert false
diff --git a/helm/software/components/cic_acic/cic2acic.mli b/helm/software/components/cic_acic/cic2acic.mli
index b63a585e6..c3cf56e88 100644
--- a/helm/software/components/cic_acic/cic2acic.mli
+++ b/helm/software/components/cic_acic/cic2acic.mli
@@ -31,7 +31,7 @@ type anntypes =
  {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
 ;;
 
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe]
 
 val string_of_sort: sort_kind -> string
 (*val sort_of_string: string -> sort_kind*)
diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml
index 6fa7cce5a..1671b98d2 100644
--- a/helm/software/components/cic_acic/doubleTypeInference.ml
+++ b/helm/software/components/cic_acic/doubleTypeInference.ml
@@ -608,15 +608,10 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
    let t1' = CicReduction.whd context t1 in
    let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
    match (t1', t2') with
-      (C.Sort _, C.Sort s2)
-        when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> 
-	 (* different from Coq manual!!! *)
-         C.Sort s2
-    | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
-	C.Sort (C.Type (CicUniv.fresh()))
-    | (C.Sort _,C.Sort (C.Type t1)) -> 
-        (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *)
-	C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
+    | (C.Sort _, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) -> C.Sort s2
+    | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->C.Sort(C.Type(CicUniv.fresh()))
+    | (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1)
+    | (C.Sort _,C.Sort (C.CProp t1)) -> C.Sort (C.CProp t1)
     | (C.Meta _, C.Sort _) -> t2'
     | (C.Meta _, (C.Meta (_,_) as t))
     | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 41c24c9ae..68afd810b 100644
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -542,7 +542,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
     | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
-    | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
+    | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
     | CicNotationPt.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
     | _ -> assert false (* god bless Bologna *)
diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml
index cd5ab3ace..c595c6d7d 100644
--- a/helm/software/components/cic_exportation/cicExportation.ml
+++ b/helm/software/components/cic_exportation/cicExportation.ml
@@ -182,7 +182,7 @@ let rec pp ~in_type t context =
          | C.Set   -> "Set"
          | C.Type _ -> "Type"
          (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
-	 | C.CProp -> "CProp" 
+	 | C.CProp _ -> "CProp" 
        )
     | C.Implicit (Some `Hole) -> "%"
     | C.Implicit _ -> "?"
diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml
index 1686cd357..58f319f4a 100644
--- a/helm/software/components/cic_proof_checking/cicPp.ml
+++ b/helm/software/components/cic_proof_checking/cicPp.ml
@@ -114,7 +114,7 @@ let rec pp t l =
          | C.Set   -> "Set"
          | C.Type _ -> "Type"
          (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
-	 | C.CProp -> "CProp" 
+	 | C.CProp _ -> "CProp" 
        )
     | C.Implicit (Some `Hole) -> "%"
     | C.Implicit _ -> "?"
@@ -347,7 +347,7 @@ let ppsort = function
   | Cic.Prop -> "Prop"
   | Cic.Set -> "Set"
   | Cic.Type _ -> "Type"
-  | Cic.CProp -> "CProp"
+  | Cic.CProp _ -> "CProp"
 
 
 (* MATITA NAMING CONVENTION *)
diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index 5e02fdbaa..1499712c9 100644
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -869,19 +869,26 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
 *)
                aux test_equality_only context t1 term' ugraph
             with  CicUtil.Subst_not_found _ -> false,ugraph)
-          (* TASSI: CONSTRAINTS *)
-        | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
+        | (C.Sort (C.Type t1), C.Sort (C.Type t2)) 
+        | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) when test_equality_only ->
             (try
               true,(CicUniv.add_eq t2 t1 ugraph)
              with CicUniv.UniverseInconsistency _ -> false,ugraph)
-          (* TASSI: CONSTRAINTS *)
-        | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+        | (C.Sort (C.Type t1), C.Sort (C.Type t2)) 
+        | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) ->
             (try
               true,(CicUniv.add_ge t2 t1 ugraph)
              with CicUniv.UniverseInconsistency _ -> false,ugraph)
-          (* TASSI: CONSTRAINTS *)
-        | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
-          (* TASSI: CONSTRAINTS *)
+        | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) when not test_equality_only ->
+            (try
+              true,(CicUniv.add_gt t2 t1 ugraph)
+             with CicUniv.UniverseInconsistency _ -> false,ugraph)
+        | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) when not test_equality_only ->
+            (try
+              true,(CicUniv.add_ge t2 t1 ugraph)
+             with CicUniv.UniverseInconsistency _ -> false,ugraph)
+        | (C.Sort s1, C.Sort (C.Type _))
+        | (C.Sort s1, C.Sort (C.CProp _)) -> (not test_equality_only),ugraph
         | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
             let b',ugraph' = aux true context s1 s2 ugraph in
diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 4dfe78301..1756497c0 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -572,11 +572,15 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
                match
                 CicReduction.whd context con_sort, CicReduction.whd [] ty_sort
                with
-                  Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2) ->
+                  Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2) 
+                | Cic.Sort (Cic.CProp u1), Cic.Sort (Cic.CProp u2) 
+                | Cic.Sort (Cic.Type u1), Cic.Sort (Cic.CProp u2) ->
                    CicUniv.add_ge u2 u1 ugraph
+                | Cic.Sort (Cic.CProp u1), Cic.Sort (Cic.Type u2) ->
+                   CicUniv.add_gt u2 u1 ugraph
                 | Cic.Sort _, Cic.Sort Cic.Prop
+                | Cic.Sort _, Cic.Sort Cic.CProp _
                 | Cic.Sort _, Cic.Sort Cic.Set
-                | Cic.Sort Cic.CProp, Cic.Sort Cic.CProp
                 | Cic.Sort _, Cic.Sort Cic.Type _ -> ugraph
                 | a,b ->
                    raise
@@ -1156,7 +1160,7 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
          ((Some (name,C.Decl so))::context) ta true
    | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph
    | (C.Sort C.Prop, C.Sort C.Set)
-   | (C.Sort C.Prop, C.Sort C.CProp)
+   | (C.Sort C.Prop, C.Sort (C.CProp _))
    | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 	 match o with
@@ -1182,12 +1186,9 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
 		       UriManager.string_of_uri uri)))
        )
    | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph
-   | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true , ugraph
    | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true , ugraph
-   | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true , ugraph
-   | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph
-   | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph
-   | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
+   | (C.Sort C.Set, C.Sort (C.Type _)) 
+   | (C.Sort C.Set, C.Sort (C.CProp _))
       when need_dummy ->
        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 	 match o with
@@ -1209,6 +1210,7 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
               UriManager.string_of_uri uri)))
        )
    | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph
+   | (C.Sort (C.CProp _), C.Sort _) when need_dummy -> true , ugraph
    | (_,_) -> false,ugraph
  in
   check_allowed_sort_elimination_aux ugraph context arity2 need_dummy
@@ -1837,9 +1839,7 @@ end;
     | (C.Sort s1, C.Sort (C.Prop | C.Set)) ->
          (* different from Coq manual!!! *)
          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
         (try
          let ugraph1 = CicUniv.add_ge t' t1 ugraph in
@@ -1847,10 +1847,32 @@ end;
           C.Sort (C.Type t'),ugraph2
         with
          CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
-    | (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.Sort (C.CProp t1), C.Sort (C.CProp t2)) -> 
+       let t' = CicUniv.fresh() in
+        (try
+         let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+         let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+          C.Sort (C.CProp t'),ugraph2
+        with
+         CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
+    | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) -> 
+       let t' = CicUniv.fresh() in
+        (try
+         let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+         let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+          C.Sort (C.CProp t'),ugraph2
+        with
+         CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
+    | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) -> 
+       let t' = CicUniv.fresh() in
+        (try
+         let ugraph1 = CicUniv.add_gt t' t1 ugraph in
+         let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+          C.Sort (C.Type t'),ugraph2
+        with
+         CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
+    | (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1),ugraph 
+    | (C.Sort _,C.Sort (C.CProp t1)) -> C.Sort (C.CProp t1),ugraph 
     | (C.Meta _, C.Sort _) -> t2',ugraph
     | (C.Meta _, (C.Meta (_,_) as t))
     | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
diff --git a/helm/software/components/cic_proof_checking/freshNamesGenerator.ml b/helm/software/components/cic_proof_checking/freshNamesGenerator.ml
index 1cb86b35a..daa0e5432 100755
--- a/helm/software/components/cic_proof_checking/freshNamesGenerator.ml
+++ b/helm/software/components/cic_proof_checking/freshNamesGenerator.ml
@@ -30,7 +30,7 @@ let debug_print = fun _ -> ()
 let rec higher_name arity =
   function 
       Cic.Sort Cic.Prop
-    | Cic.Sort Cic.CProp -> 
+    | Cic.Sort (Cic.CProp _) -> 
 	if arity = 0 then "A" (* propositions *)
 	else if arity = 1 then "P" (* predicates *)
 	else "R" (*relations *)
@@ -87,7 +87,7 @@ let mk_fresh_name ~subst metasenv context name ~typ =
         in 
          (match ty with
              C.Sort C.Prop
-           | C.Sort C.CProp -> "H"
+           | C.Sort (C.CProp _) -> "H"
            | _ -> guess_a_name context typ
          )
         with CicTypeChecker.TypeCheckerFailure _ -> "H"
diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index a1a7bdea8..b5204de02 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1065,8 +1065,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
     let t1'' = CicReduction.whd ~subst context t1 in
     let t2'' = CicReduction.whd ~subst context_for_t2 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 s2) when (s2 = C.Prop || s2 = C.Set) -> 
               (* different than Coq manual!!! *)
               C.Sort s2,subst,metasenv,ugraph
         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
@@ -1077,8 +1076,34 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                 C.Sort (C.Type t'),subst,metasenv,ugraph2
               with
                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+        | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) -> 
+            let t' = CicUniv.fresh() in 
+             (try
+              let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+              let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+                C.Sort (C.CProp t'),subst,metasenv,ugraph2
+              with
+               CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+        | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) -> 
+            let t' = CicUniv.fresh() in 
+             (try
+              let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+              let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+                C.Sort (C.CProp t'),subst,metasenv,ugraph2
+              with
+               CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+        | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) -> 
+            let t' = CicUniv.fresh() in 
+             (try
+              let ugraph1 = CicUniv.add_gt t' t1 ugraph in
+              let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+                C.Sort (C.Type t'),subst,metasenv,ugraph2
+              with
+               CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
         | (C.Sort _,C.Sort (C.Type t1)) -> 
             C.Sort (C.Type t1),subst,metasenv,ugraph
+        | (C.Sort _,C.Sort (C.CProp t1)) -> 
+            C.Sort (C.CProp t1),subst,metasenv,ugraph
         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
             (* TODO how can we force the meta to become a sort? If we don't we
diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 5aac1ef7d..bae4a8f59 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -427,7 +427,7 @@ EXTEND
     [ "Prop" -> `Prop
     | "Set" -> `Set
     | "Type" -> `Type (CicUniv.fresh ()) 
-    | "CProp" -> `CProp
+    | "CProp" -> `CProp (CicUniv.fresh ())
     ]
   ];
   explicit_subst: [
diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 0f51e36a9..1ee406623 100644
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -100,7 +100,7 @@ let binder_symbol s =
 let string_of_sort_kind = function
   | `Prop -> "Prop"
   | `Set -> "Set"
-  | `CProp -> "CProp"
+  | `CProp _ -> "CProp"
   | `Type _ -> "Type"
 
 let pp_ast0 t k =
diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 37f0939bd..c3e2b6b48 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -30,6 +30,14 @@ let debug = false;;
 let debug_print s = 
   if debug then prerr_endline (Lazy.force s);;
 
+let is_propositional context sort = 
+  match CicReduction.whd context sort with
+  | Cic.Sort Cic.Prop 
+  | Cic.Sort (Cic.CProp _) -> true
+  | _-> false
+;;
+
+
 type auto_params = Cic.term list * (string * string) list 
 
 let elems = ref [] ;;
@@ -133,11 +141,7 @@ let is_unit_equation context metasenv oldnewmeta term =
             CicTypeChecker.type_of_aux' metasenv context mt 
               CicUniv.oblivion_ugraph
           in
-          let b, _ = 
-            CicReduction.are_convertible ~metasenv context 
-              sort (Cic.Sort Cic.Prop) u
-          in
-          if b then Some i else None 
+          if is_propositional context sort then Some i else None 
       | _ -> assert false)
     args
   in
@@ -314,11 +318,7 @@ let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.u
             CicTypeChecker.type_of_aux' metasenv context mt 
               CicUniv.oblivion_ugraph
           in
-          let b, _ = 
-            CicReduction.are_convertible ~metasenv context 
-              sort (Cic.Sort Cic.Prop) u
-          in
-          if b then Some i else None 
+          if is_propositional context sort then Some i else None 
       | _ -> assert false)
     args
   in
@@ -686,7 +686,7 @@ let ppterm ctx t =
 ;;
 let is_in_prop context subst metasenv ty =
   let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
-  fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
+  is_propositional context sort
 ;;
 
 let assert_proof_is_valid proof metasenv context goalty =
@@ -723,10 +723,7 @@ let split_goals_in_prop metasenv subst gl =
       let _,context,ty = CicUtil.lookup_meta g metasenv in
       try
         let sort,u = typeof ~subst metasenv context ty ugraph in
-        let b,_ = 
-          CicReduction.are_convertible 
-            ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in
-        b
+        is_propositional context sort
       with 
       | CicTypeChecker.AssertFailure s 
       | CicTypeChecker.TypeCheckerFailure s -> 
diff --git a/helm/software/components/tactics/eliminationTactics.ml b/helm/software/components/tactics/eliminationTactics.ml
index 6e0c223d2..5a293bcaf 100644
--- a/helm/software/components/tactics/eliminationTactics.ml
+++ b/helm/software/components/tactics/eliminationTactics.ml
@@ -155,7 +155,7 @@ let warn s = debug_print (lazy ("DECOMPOSE: " ^ (Lazy.force s)))
 
 (* roba seria ------------------------------------------------------------- *)
 
-let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort C.CProp]) 
+let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort (C.CProp (CicUniv.fresh ()))]) 
                   ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
    let decompose_tac status =
       let (proof, goal) = status in
diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index 53bfc39a9..3822b7eac 100644
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -646,7 +646,7 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
        match ty_ty with
           C.Sort C.Prop -> "_ind"
         | C.Sort C.Set  -> "_rec"
-        | C.Sort C.CProp -> "_rec"
+        | C.Sort (C.CProp _) -> "_rect"
         | C.Sort (C.Type _)-> "_rect" 
         | C.Meta (_,_) -> raise TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
         | _ -> assert false
diff --git a/helm/software/matita/dist/ChangeLog b/helm/software/matita/dist/ChangeLog
index e171b8386..a7a7e0ce1 100644
--- a/helm/software/matita/dist/ChangeLog
+++ b/helm/software/matita/dist/ChangeLog
@@ -1,6 +1,7 @@
 0.5.?  - ?/?/? - ?
 	* refinement of match fixed to prevent useless unfolding,
 	  head_beta_reduce is used instead of whd ~delta:true
+	* CProp hierarchy, interleaved with type (used to be a single universe)
 
 0.5.1  - 29/5/2008 - minor bug fix release
 	* visualization of inductive types reports the number of fixed parameters
diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index a27b01831..9e0f85b58 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -247,7 +247,7 @@ let cic2grafite context menv t =
       | Cic.Meta _ -> PT.Implicit
       | Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
       | Cic.Sort Cic.Set -> PT.Sort `Set
-      | Cic.Sort Cic.CProp -> PT.Sort `CProp
+      | Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u)
       | Cic.Sort Cic.Prop -> PT.Sort `Prop
       | _ as t -> PT.Ident ("ERROR: "^CicPp.ppterm t, None)
     in