From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 21 Sep 2009 10:01:28 +0000 (+0000)
Subject: huge commit regarding universes:
X-Git-Tag: make_still_working~3455
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8b1a49bbee9eea86eb74c040defe701370ca5893;p=helm.git

huge commit regarding universes:
- only Type[foo] can be declare with a strict (<) constraint among other
  Type[bar]
- CProp[foo] is automatically available for Type[foo]
- The CProp hierarchy can be collapsed (hopefully in a consistent way)
  to both Prop OR Type:
  - You cannot eliminate CProp to build a Type like for Prop/Type
  - You cannot eliminate Prop to build a CProp, like for Prop/Type
- Peculiarity: CProp[i] has type Type[i+1], since CProp[i+1] is only >=
  of CProp[i] to allow collapsing them (while < whould be violated).

New function to delift a type w.r.t. a term list, to potentially build a
dependent type, used in lambda_intro and Letin expected type propagation.
---

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 1a664d525..829e78b6d 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -581,9 +581,9 @@ EXTEND
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
-    | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n
+    | "Type"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NType n
     | "Type" -> `Type (CicUniv.fresh ()) 
-    | "CProp"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NCProp n
+    | "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NCProp n
     | "CProp" -> `CProp (CicUniv.fresh ())
     ]
   ];
diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 5c8f461c1..68350ac75 100644
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -219,7 +219,7 @@ type ('term,'obj) command =
 type ncommand =
   | UnificationHint of loc * CicNotationPt.term * int (* term, precedence *)
   | NObj of loc * CicNotationPt.term CicNotationPt.obj
-  | NUnivConstraint of loc * bool * NUri.uri * NUri.uri
+  | NUnivConstraint of loc * NUri.uri * NUri.uri
   | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
   | NCoercion of loc * string *
       CicNotationPt.term * CicNotationPt.term *
diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index ec9f3866f..482a138a6 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -501,25 +501,25 @@ let eval_unification_hint status t n =
   status,`New []
 ;;
 
-let basic_eval_add_constraint (s,u1,u2) status =
- NCicLibrary.add_constraint status s u1 u2
+let basic_eval_add_constraint (u1,u2) status =
+ NCicLibrary.add_constraint status u1 u2
 ;;
 
 let inject_constraint =
- let basic_eval_add_constraint (s,u1,u2) 
+ let basic_eval_add_constraint (u1,u2) 
        ~refresh_uri_in_universe 
        ~refresh_uri_in_term
  =
   let u1 = refresh_uri_in_universe u1 in 
   let u2 = refresh_uri_in_universe u2 in 
-  basic_eval_add_constraint (s,u1,u2)
+  basic_eval_add_constraint (u1,u2)
  in
   NRstatus.Serializer.register "constraints" basic_eval_add_constraint
 ;;
 
-let eval_add_constraint status s u1 u2 = 
- let status = basic_eval_add_constraint (s,u1,u2) status in
- let dump = inject_constraint (s,u1,u2)::status#dump in
+let eval_add_constraint status u1 u2 = 
+ let status = basic_eval_add_constraint (u1,u2) status in
+ let dump = inject_constraint (u1,u2)::status#dump in
  let status = status#set_dump dump in
   status,`Old []
 ;;
@@ -774,9 +774,9 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                 in
                 status, concat_nuris uris nuris
                with
-                NCicTypeChecker.TypeCheckerFailure msg
-                 when Lazy.force msg =
-                 "Sort elimination not allowed" ->
+               | MultiPassDisambiguator.DisambiguationError _ 
+               | NCicTypeChecker.TypeCheckerFailure _ ->
+                  HLog.warn "error in generating projection/eliminator";
                   status,uris
              ) (status,`New [] (* uris *)) boxml in
            let coercions =
@@ -791,17 +791,21 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
            let status,uris =
             List.fold_left
              (fun (status,uris) (name,cpos,arity) ->
-               let metasenv,subst,status,t =
-                GrafiteDisambiguate.disambiguate_nterm None status [] [] []
-                 ("",0,CicNotationPt.Ident (name,None)) in
-               assert (metasenv = [] && subst = []);
-               let status, nuris = 
-                 NCicCoercDeclaration.
-                   basic_eval_and_record_ncoercion_from_t_cpos_arity 
-                    status (name,t,cpos,arity)
-               in
-               let uris = concat_nuris nuris uris in
-               status, uris) 
+               try
+                 let metasenv,subst,status,t =
+                  GrafiteDisambiguate.disambiguate_nterm None status [] [] []
+                   ("",0,CicNotationPt.Ident (name,None)) in
+                 assert (metasenv = [] && subst = []);
+                 let status, nuris = 
+                   NCicCoercDeclaration.
+                     basic_eval_and_record_ncoercion_from_t_cpos_arity 
+                      status (name,t,cpos,arity)
+                 in
+                 let uris = concat_nuris nuris uris in
+                 status, uris
+               with MultiPassDisambiguator.DisambiguationError _-> 
+                 HLog.warn ("error in generating coercion: "^name);
+                 status, uris) 
              (status,uris) coercions
            in
             status,uris
@@ -857,8 +861,8 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           [] ->
            eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
         | _ -> status,`New [])
-  | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) ->
-      eval_add_constraint status strict [false,u1] [false,u2]
+  | GrafiteAst.NUnivConstraint (loc,u1,u2) ->
+      eval_add_constraint status [`Type,u1] [`Type,u2]
 ;;
 
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status
diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index c9ece6dba..bf34fc283 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -817,26 +817,15 @@ EXTEND
         in
         G.NObj (loc, N.Inductive (params, ind_types))
     | IDENT "universe"; IDENT "constraint"; u1 = tactic_term; 
-        strict = [ SYMBOL <:unicode<lt>> -> true 
-                 | SYMBOL <:unicode<leq>> -> false ]; 
-        u2 = tactic_term ->
-        let u1 =
-          match u1 with
+        SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
+        let urify = function 
           | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
               NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
-          | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
-              NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
-          | _ -> raise (Failure "only a sort can be constrained")
+          | _ -> raise (Failure "only a Type[…] sort can be constrained")
         in
-        let u2 =
-          match u2 with
-          | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
-              NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
-          | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
-              NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
-          | _ -> raise (Failure "only a sort can be constrained")
-        in
-         G.NUnivConstraint (loc, strict,u1,u2)
+        let u1 = urify u1 in
+        let u2 = urify u2 in
+         G.NUnivConstraint (loc,u1,u2)
     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
         G.UnificationHint (loc, t, n)
     | IDENT "ncoercion"; name = IDENT; SYMBOL ":"; ty = term; 
diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 4bfeab669..6bf1c05ba 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -64,7 +64,7 @@ let refine_term
 ;;
 
 let refine_obj 
-  ~rdb metasenv subst context _uri 
+  ~rdb metasenv subst _context _uri 
   ~use_coercions obj _ _ugraph ~localization_tbl 
 =
   assert (metasenv=[]);
@@ -72,7 +72,6 @@ let refine_obj
   let localise t = 
     try NCicUntrusted.NCicHash.find localization_tbl t
     with Not_found -> 
-      prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
       (*assert false*)HExtlib.dummy_floc
   in
   try
@@ -322,7 +321,7 @@ let interpretate_term_and_interpretate_term_option
        with Not_found -> 
          try NCic.Const (List.assoc name obj_context)
          with Not_found ->
-           Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
+            Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
     | CicNotationPt.Uri (uri, subst) ->
        assert (subst = None);
        (try
@@ -344,15 +343,15 @@ let interpretate_term_and_interpretate_term_option
          NCic.Meta (index, (0, NCic.Ctx cic_subst))
     | CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop
     | CicNotationPt.Sort `Set -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
+       [`Type,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
     | CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string "cic:/matita/pts/Type0.univ"])
+       [`Type,NUri.uri_of_string "cic:/matita/pts/Type0.univ"])
     | CicNotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
+       [`Type,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
     | CicNotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string ("cic:/matita/pts/CProp" ^ s ^ ".univ")])
+       [`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
     | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string "cic:/matita/pts/CProp0.univ"])
+       [`CProp,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
     | CicNotationPt.Symbol (symbol, instance) ->
         Disambiguate.resolve ~env ~mk_choice 
          (Symbol (symbol, instance)) (`Args [])
diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index f5fb6841c..8f014d4d2 100644
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -53,15 +53,15 @@ let logger =
 
 let mk_type n = 
   if n = 0 then
-     [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
+     [`Type, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
   else
-     [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+     [`Type, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 let mk_cprop n = 
   if n = 0 then 
-    [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
+    [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
   else
-    [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
+    [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 
 
@@ -151,16 +151,9 @@ let _ =
     try
     let rec aux = function
       | a::(b::_ as tl) ->
-         NCicEnvironment.add_constraint true (mk_type a) (mk_type b);
-         NCicEnvironment.add_constraint true (mk_cprop a) (mk_cprop b);
-         NCicEnvironment.add_constraint true (mk_cprop a) (mk_type b);
-         NCicEnvironment.add_constraint true (mk_type a) (mk_cprop b);
-         NCicEnvironment.add_constraint false (mk_cprop a) (mk_type a);
-         NCicEnvironment.add_constraint false (mk_type a) (mk_cprop a);
+         NCicEnvironment.add_lt_constraint (mk_type a) (mk_type b);
+         NCicEnvironment.add_lt_constraint (mk_type a) (mk_cprop b);
          aux tl
-      | [a] -> 
-         NCicEnvironment.add_constraint false (mk_type a) (mk_cprop a);
-         NCicEnvironment.add_constraint false (mk_cprop a) (mk_type a);
       | _ -> ()
     in
        aux lll
diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml
index e52042216..c531d1c2b 100644
--- a/helm/software/components/ng_kernel/nCic.ml
+++ b/helm/software/components/ng_kernel/nCic.ml
@@ -13,7 +13,9 @@
 
 (********************************* TERMS ************************************)
 
-type universe = (bool * NUri.uri) list 
+type univ_algebra = [ `Type | `Succ | `CProp ]
+
+type universe = (univ_algebra * NUri.uri) list 
   (* Max of non-empty list of named universes, or their successor (when true) 
    * The empty list represents type0 *)
 
diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_kernel/nCic2OCic.ml
index 5f8279d7e..1006d03c6 100644
--- a/helm/software/components/ng_kernel/nCic2OCic.ml
+++ b/helm/software/components/ng_kernel/nCic2OCic.ml
@@ -15,7 +15,7 @@ let ouri_of_nuri u = UriManager.uri_of_string (NUri.string_of_uri u);;
 
 let ouri_of_reference (NReference.Ref (u,_)) = ouri_of_nuri u;;
 
-let cprop = [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")];;
+let cprop = [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")];;
 
 let nn_2_on = function
   | "_" -> Cic.Anonymous
diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index b3b1eda16..893e514b1 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -29,91 +29,177 @@ let set_get_obj f = get_obj := f;;
 
 let type0 = []
 
-let max l1 l2 =
- HExtlib.list_uniq ~eq:(fun (b1,u1) (b2,u2) -> b1=b2 && NUri.eq u1 u2)
-  (List.sort (fun (b1,u1) (b2,u2) ->
-    let res = compare b1 b2 in if res = 0 then NUri.compare u1 u2 else res)
-      (l1 @ l2))
+module F = Format 
+
+let rec ppsort f = function
+  | C.Prop -> F.fprintf f "Prop"
+  | (C.Type []) -> F.fprintf f "Type0"
+  | (C.Type [`Type, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)
+  | (C.Type [`Succ, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u)
+  | (C.Type [`CProp, u]) -> F.fprintf f "P(%s)" (NUri.name_of_uri u)
+  | (C.Type l) -> 
+      F.fprintf f "Max(";
+      ppsort f ((C.Type [List.hd l]));
+      List.iter (fun x -> F.fprintf f ",";ppsort f ((C.Type [x]))) (List.tl l);
+      F.fprintf f ")"
+;;
 
-let le_constraints = ref [] (* strict,a,b *)
+let string_of_univ u =
+  let b = Buffer.create 100 in
+  let f = Format.formatter_of_buffer b in
+  ppsort f (NCic.Type u);
+  Format.fprintf f "@?";
+  Buffer.contents b
+;;
 
-let rec le_path_uri avoid strict a b =
- (not strict && NUri.eq a b) ||
- List.exists
-  (fun (strict',x,y) ->
-     NUri.eq y b && not (List.exists (NUri.eq x) avoid) &&
-       le_path_uri (x::avoid) (strict && not strict') a x
-  ) !le_constraints
+let eq_univ (b1,u1) (b2,u2) = b1=b2 && NUri.eq u1 u2;;
+
+let max (l1:NCic.universe) (l2:NCic.universe) =
+ match l2 with
+ | x::tl -> 
+    let rest = List.filter (fun y -> not (eq_univ x y)) (l1@tl) in
+    x :: HExtlib.list_uniq ~eq:eq_univ
+      (List.sort (fun (b1,u1) (b2,u2) ->
+         let res = compare b1 b2 in 
+         if res = 0 then NUri.compare u1 u2 else res)
+      rest)
+ | [] -> 
+     match l1 with
+     | [] -> []
+     | ((`Type|`Succ), _)::_ -> l1
+     | (`CProp, u)::tl -> (`Type, u)::tl
 ;;
 
-let leq_path a b = le_path_uri [b] (fst a) (snd a) b;;
+let lt_constraints = ref [] (* a,b := a < b *)
 
-let universe_leq a b = 
-  match a, b with
-  | a,[(false,b)] -> List.for_all (fun a -> leq_path a b) a
-  | _,_ ->
-     raise (BadConstraint
-      (lazy "trying to check if a universe is less or equal than an inferred universe"))
+let rec lt_path_uri avoid a b = 
+ List.exists
+  (fun (x,y) ->
+      NUri.eq y b && 
+     (NUri.eq a x ||
+        (not (List.exists (NUri.eq x) avoid) &&
+        lt_path_uri (x::avoid) a x))
+  ) !lt_constraints
+;;
+
+let lt_path a b = lt_path_uri [b] a b;;
 
 let universe_eq a b = 
   match a,b with 
-  | [(false,_)], [(false,_)] -> universe_leq b a && universe_leq a b
-  | _, [(false,_)]
-  | [(false,_)],_ -> false
+  | [(`Type|`CProp) as b1, u1], [(`Type|`CProp) as b2, u2] -> 
+         b1 = b2 && NUri.eq u1 u2
+  | _, [(`Type|`CProp),_]
+  | [(`Type|`CProp),_],_ -> false
   | _ ->
      raise (BadConstraint
       (lazy "trying to check if two inferred universes are equal"))
 ;;
 
-let pp_constraint b x y =  
-  NUri.name_of_uri x ^ (if b then " < " else " <= ") ^ NUri.name_of_uri y
+let universe_leq a b = 
+  match a, b with
+  | (((`Type|`Succ),_)::_ | []) , [`CProp,_] -> false
+  | l, [((`Type|`CProp),b)] -> 
+       List.for_all 
+         (function 
+         | `Succ,a -> lt_path a b 
+         | _, a -> NUri.eq a b || lt_path a b) l
+  | _, ([] | [`Succ,_] | _::_::_) -> 
+     raise (BadConstraint (lazy (
+       "trying to check if "^string_of_univ a^
+       " is leq than the inferred universe " ^ string_of_univ b)))
+;;
+
+let are_sorts_convertible ~test_eq_only s1 s2 =
+   match s1,s2 with
+   | C.Type a, C.Type b when not test_eq_only -> universe_leq a b
+   | C.Type a, C.Type b -> universe_eq a b
+   | C.Prop,C.Type _ -> (not test_eq_only)
+   | C.Prop, C.Prop -> true
+   | _ -> false
+;;
+
+let pp_constraint x y =  
+  NUri.name_of_uri x ^ " < " ^ NUri.name_of_uri y
 ;;
 
 let pp_constraints () =
-  String.concat "\n" (List.map (fun (b,x,y) -> pp_constraint b x y) !le_constraints)
+  String.concat "\n" (List.map (fun (x,y) -> pp_constraint x y) !lt_constraints)
 ;;
 
 let universes = ref [];;
 
-let get_universes () = List.map (fun x -> [false,x]) !universes;;
+let get_universes () = 
+  List.map (fun x -> [`Type,x]) !universes @
+  List.map (fun x -> [`CProp,x]) !universes
+;;
 
 let is_declared u =
  match u with
-    [false,x] -> List.exists (fun y -> NUri.eq x y) !universes
-  | _ -> assert false
+ | [(`CProp|`Type),x] -> List.exists (fun y -> NUri.eq x y) !universes
+ | _ -> assert false
+;;
+
+exception UntypableSort of string Lazy.t
+exception AssertFailure of string Lazy.t
+
+let typeof_sort = function
+  | C.Type ([(`Type|`CProp),u] as univ) ->
+     if is_declared univ then (C.Type [`Succ, u])
+     else 
+       raise (UntypableSort (lazy ("undeclared universe " ^
+         NUri.string_of_uri u ^ "\ndeclared ones are: " ^ 
+         String.concat ", " (List.map NUri.string_of_uri !universes)
+     )))
+  | C.Type t -> 
+      raise (AssertFailure (lazy (
+              "Cannot type an inferred type: "^ string_of_univ t)))
+  | C.Prop -> (C.Type type0)
 ;;
 
-let add_constraint strict a b = 
+let add_lt_constraint a b = 
   match a,b with
-  | [false,a2],[false,b2] -> 
-      if not (le_path_uri [] strict a2 b2) then (
-        if le_path_uri [] (not strict) b2 a2 then
-         (raise(BadConstraint(lazy("universe inconsistency adding "^pp_constraint strict a2 b2
+  | [`Type,a2],[`Type,b2] -> 
+      if not (lt_path_uri [] a2 b2) then (
+        if lt_path_uri [] b2 a2 || NUri.eq a2 b2 then
+         (raise(BadConstraint(lazy("universe inconsistency adding "^
+                    pp_constraint a2 b2
            ^ " to:\n" ^ pp_constraints ()))));
         universes := a2 :: b2 :: 
           List.filter (fun x -> not (NUri.eq x a2 || NUri.eq x b2)) !universes;
-        le_constraints := (strict,a2,b2) :: !le_constraints);
-        history := (`Constr (strict,a,b))::!history;
+        lt_constraints := (a2,b2) :: !lt_constraints);
+      history := (`Constr (a,b))::!history;
   | _ -> raise (BadConstraint
           (lazy "trying to add a constraint on an inferred universe"))
 ;;
 
 let sup l =
   match l with
-  | [false,_] -> Some l
+  | [(`Type|`CProp),_] -> Some l
   | l ->
-   let bigger_than acc (s1,n1) = List.filter (le_path_uri [] s1 n1) acc in
+   let bigger_than acc (_s1,n1) = 
+     List.filter (fun x -> lt_path_uri [] n1 x || NUri.eq n1 x) acc 
+   in
    let solutions = List.fold_left bigger_than !universes l in
+   let fam = match l with (`CProp,_)::_ -> `CProp | _ -> `Type in
    let rec aux = function
      | [] -> None
      | u :: tl ->
-         if List.exists (fun x -> le_path_uri [] true x u) solutions then aux tl
-         else Some [false,u]
+         if List.exists (fun x -> lt_path_uri [] x u) solutions then aux tl
+         else Some [fam,u]
    in
     aux solutions
 ;;
 
+let allowed_sort_elimination s1 s2 =
+  match s1, s2 with
+  | C.Type (((`Type|`Succ),_)::_ | []), C.Type (((`Type|`Succ),_)::_ | []) 
+  | C.Type _, C.Type ((`CProp,_)::_) 
+  | C.Type _, C.Prop
+  | C.Prop, C.Prop -> `Yes
 
+  | C.Type ((`CProp,_)::_), C.Type (((`Type|`Succ),_)::_ | [])
+  | C.Prop, C.Type _ -> `UnitOnly
+;;
 
 let typecheck_obj,already_set = ref (fun _ -> assert false), ref false;;
 let set_typecheck_obj f =
@@ -144,10 +230,10 @@ let invalidate_item item =
    List.iter 
      (function 
      | `Obj (uri,_) -> NUri.UriHash.remove cache uri
-     | `Constr (strict,[_,u1],[_,u2]) as c -> 
-          let w = strict,u1,u2 in
+     | `Constr ([_,u1],[_,u2]) as c -> 
+          let w = u1,u2 in
           if not(List.mem c !history) then 
-           le_constraints := List.filter ((<>) w) !le_constraints;
+           lt_constraints := List.filter ((<>) w) !lt_constraints;
      | `Constr _ -> assert false
      ) to_be_deleted
 ;;
diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli
index 778931706..35b97aa59 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.mli
+++ b/helm/software/components/ng_kernel/nCicEnvironment.mli
@@ -14,7 +14,6 @@
 exception CircularDependency of string Lazy.t;;
 exception ObjectNotFound of string Lazy.t;;
 exception BadDependency of string Lazy.t * exn;;
-exception BadConstraint of string Lazy.t;;
 exception AlreadyDefined of string Lazy.t;;
 
 val set_get_obj: (NUri.uri -> NCic.obj) -> unit
@@ -25,21 +24,6 @@ val check_and_add_obj: NCic.obj -> unit
 
 val get_relevance: NReference.reference -> bool list
 
-val type0: NCic.universe
-val get_universes: unit -> NCic.universe list
-val is_declared: NCic.universe -> bool
-val max: NCic.universe -> NCic.universe -> NCic.universe
-(* universe_* raise BadConstraints if the second arg. is an inferred universe *)
-val universe_eq: NCic.universe -> NCic.universe -> bool
-val universe_leq: NCic.universe -> NCic.universe -> bool
-(* add_constraint raise BadConstraint in case of universe inconsistency
-   or if the second argument is an inferred universe
-   true -> strict check (<); false -> loose check (<=)
-*)
-val add_constraint: bool -> NCic.universe -> NCic.universe -> unit
-val sup : NCic.universe -> NCic.universe option
-val pp_constraints: unit -> string
-
 val get_checked_def:
   NReference.reference -> 
     NCic.relevance * string * NCic.term * NCic.term * NCic.c_attr * int
@@ -56,10 +40,46 @@ val get_checked_fixes_or_cofixes:
 (* invalidate the object and all those that entered the environment after it *)
 val invalidate_item: 
       [ `Obj of NUri.uri * NCic.obj 
-      | `Constr of bool * NCic.universe * NCic.universe ] -> unit
+      | `Constr of NCic.universe * NCic.universe ] -> unit
 
 val invalidate: unit -> unit
 
 val set_typecheck_obj: (NCic.obj -> unit) -> unit
 
+(* =========== universes ============= *)
+
+(* utils *)
+val ppsort : Format.formatter -> NCic.sort -> unit
+val pp_constraints: unit -> string
+val get_universes: unit -> NCic.universe list
+
+(* The type of Prop, smaller than any other type *)
+val type0: NCic.universe
+
+(* use to type products *)
+val max: NCic.universe -> NCic.universe -> NCic.universe
+
+(* raise BadConstraints if the second arg. is an inferred universe or
+ * if the added constraint gives circularity *)
+exception BadConstraint of string Lazy.t;;
+val add_lt_constraint: NCic.universe -> NCic.universe -> unit
+val universe_eq: NCic.universe -> NCic.universe -> bool
+val universe_leq: NCic.universe -> NCic.universe -> bool
+
+(* checks if s1 <= s2 *)
+val are_sorts_convertible: test_eq_only:bool -> NCic.sort -> NCic.sort -> bool
+
+(* to type a Match *)
+val allowed_sort_elimination: NCic.sort -> NCic.sort -> [ `Yes | `UnitOnly ]
+
+(* algebraic successor function *)
+exception UntypableSort of string Lazy.t
+exception AssertFailure of string Lazy.t
+val typeof_sort: NCic.sort -> NCic.sort
+
+(* looks for a declared universe that is the least one above the input *)
+val sup : NCic.universe -> NCic.universe option
+
+(* =========== /universes ============= *)
+
 (* EOF *)
diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index 9a2842e0e..e7d7c3b11 100644
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -74,7 +74,7 @@ let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";;
 
 type timestamp =
  [ `Obj of NUri.uri * NCic.obj 
- | `Constr of bool * NCic.universe * NCic.universe] list *
+ | `Constr of NCic.universe * NCic.universe] list *
  (NUri.uri * string * NReference.reference) list *
  NCic.obj NUri.UriMap.t *
  NUri.uri list
@@ -310,9 +310,9 @@ let add_obj status ((u,_,_,_,_) as obj) =
   status#set_timestamp (!storage,!local_aliases,!cache,!includes)
 ;;
 
-let add_constraint status strict u1 u2 = 
-  NCicEnvironment.add_constraint strict u1 u2;
-  storage := (`Constr (strict,u1,u2)) :: !storage;
+let add_constraint status u1 u2 = 
+  NCicEnvironment.add_lt_constraint u1 u2;
+  storage := (`Constr (u1,u2)) :: !storage;
   status#set_timestamp (!storage,!local_aliases,!cache,!includes)
 ;;
 
diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli
index d89db9d71..6dc7dde43 100644
--- a/helm/software/components/ng_kernel/nCicLibrary.mli
+++ b/helm/software/components/ng_kernel/nCicLibrary.mli
@@ -30,7 +30,7 @@ class status :
 (* it also checks it and add it to the environment *)
 val add_obj: #status as 'status -> NCic.obj -> 'status
 val add_constraint: 
-  #status as 'status -> bool -> NCic.universe -> NCic.universe -> 'status
+  #status as 'status -> NCic.universe -> NCic.universe -> 'status
 val aliases_of: NUri.uri -> NReference.reference list
 val resolve: string -> NReference.reference list
 (* warning: get_obj may raise (NCicEnvironment.ObjectNotFoud l) *)
diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 2f4b694de..12227b4b1 100644
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -173,16 +173,7 @@ let ppterm ~formatter:f ~context ~subst ~metasenv:_ ?(inside_fix=false) t =
             (List.map (NCicSubstitution.lift shift) (List.tl l));
          end;
        F.fprintf f "])"
-  | C.Sort C.Prop -> F.fprintf f "Prop"
-  | C.Sort (C.Type []) -> F.fprintf f "Type0"
-  | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)
-  | C.Sort (C.Type [true, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u)
-  | C.Sort (C.Type l) -> 
-      F.fprintf f "Max(";
-      aux ctx (C.Sort (C.Type [List.hd l]));
-      List.iter (fun x -> F.fprintf f ",";aux ctx (C.Sort (C.Type [x])))
-       (List.tl l);
-      F.fprintf f ")"
+  | C.Sort s -> NCicEnvironment.ppsort f s
  in 
   aux ~toplevel:true (List.map fst context) t
 ;;
diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 432ea9a45..a88a1aaf3 100644
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -213,12 +213,8 @@ let alpha_eq ~test_lambda_source aux test_eq_only metasenv subst context t1 t2 =
    true
  else
    match (t1,t2) with
-   | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> 
-       NCicEnvironment.universe_leq a b
-   | (C.Sort (C.Type a), C.Sort (C.Type b)) -> 
-       NCicEnvironment.universe_eq a b
-   | (C.Sort C.Prop,C.Sort (C.Type _)) -> (not test_eq_only)
-   | (C.Sort C.Prop, C.Sort C.Prop) -> true
+   | C.Sort s1, C.Sort s2 -> 
+       NCicEnvironment.are_sorts_convertible ~test_eq_only s1 s2 
 
    | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
        aux true context s1 s2 &&
diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 6dbaf3e5d..0b4b95eba 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -395,16 +395,11 @@ let rec typeof ~subst ~metasenv context term =
         with Failure _ -> 
           raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n
             ^" under: " ^ NCicPp.ppcontext ~metasenv ~subst context))))
-    | C.Sort (C.Type ([false,u] as univ)) ->
-       if NCicEnvironment.is_declared univ then
-        C.Sort (C.Type [true, u])
-       else
-        raise (TypeCheckerFailure (lazy ("undeclared universe " ^
-         NUri.string_of_uri u)))
-    | C.Sort (C.Type _) -> 
-        raise (AssertFailure (lazy ("Cannot type an inferred type: "^
-          NCicPp.ppterm ~subst ~metasenv ~context t)))
-    | C.Sort _ -> C.Sort (C.Type NCicEnvironment.type0)
+    | C.Sort s -> 
+         (try C.Sort (NCicEnvironment.typeof_sort s) 
+         with 
+         | NCicEnvironment.UntypableSort msg -> raise (TypeCheckerFailure msg)
+         | NCicEnvironment.AssertFailure msg -> raise (AssertFailure msg))
     | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
     | C.Meta (n,l) as t -> 
        let canonical_ctx,ty =
@@ -664,9 +659,10 @@ and check_allowed_sort_elimination ~subst ~metasenv r =
            (PP.ppterm ~subst ~metasenv ~context so)
            )));
          (match arity1, R.whd ~subst ((name,C.Decl so)::context) ta with
-           | (C.Sort C.Type _, C.Sort _)
-           | (C.Sort C.Prop, C.Sort C.Prop) -> ()
-           | (C.Sort C.Prop, C.Sort C.Type _) ->
+           | C.Sort s1, C.Sort s2 ->
+               (match NCicEnvironment.allowed_sort_elimination s1 s2 with
+               | `Yes -> ()
+               | `UnitOnly ->
        (* TODO: we should pass all these parameters since we
         * have them already *)
                let _,leftno,itl,_,i = E.get_checked_indtys r in
@@ -684,8 +680,8 @@ and check_allowed_sort_elimination ~subst ~metasenv r =
                      is_non_informative ~metasenv ~subst leftno constrty))
                 then
                  raise (TypeCheckerFailure (lazy
-                  ("Sort elimination not allowed")));
-         | _,_ -> ())
+                  ("Sort elimination not allowed"))))
+           | _ -> ())
       | _,_ -> ()
   in
    aux 
@@ -742,7 +738,9 @@ and is_non_informative ~metasenv ~subst paramsno c =
    match R.whd ~subst context c with
     | C.Prod (n,so,de) ->
        let s = typeof ~metasenv ~subst context so in
-       s = C.Sort C.Prop && aux ((n,(C.Decl so))::context) de
+       (s = C.Sort C.Prop || 
+        match s with C.Sort (C.Type ((`CProp,_)::_)) -> true | _ -> false) && 
+       aux ((n,(C.Decl so))::context) de
     | _ -> true in
  let context',dx = NCicReduction.split_prods ~subst [] paramsno c in
   aux context' dx
diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 225269b70..7bfb6c39c 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -16,14 +16,14 @@ module Ref = NReference
 let nuri_of_ouri o = NUri.uri_of_string (UriManager.string_of_uri o);;
 
 let mk_type n = 
- [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+ [`Type, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 
 let mk_cprop n = 
   if n = 0 then 
-    [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
+    [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
   else
-    [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
+    [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 
 let is_proof_irrelevant context ty =
diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index d98aa8b18..0dbd6260a 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -350,7 +350,7 @@ module Paramod (B : Orderings.Blob) = struct
   ;;
 
   let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
-    let initial_timestamp = Unix.gettimeofday () in
+    let _initial_timestamp = Unix.gettimeofday () in
     let passives =
       add_passive_clauses ~no_weight:true passive_empty_set passives
     in
diff --git a/helm/software/components/ng_refiner/.depend.opt b/helm/software/components/ng_refiner/.depend.opt
index dc9a46fb3..35146bcc8 100644
--- a/helm/software/components/ng_refiner/.depend.opt
+++ b/helm/software/components/ng_refiner/.depend.opt
@@ -2,7 +2,7 @@ nDiscriminationTree.cmi:
 nCicMetaSubst.cmi: 
 nCicUnifHint.cmi: 
 nCicCoercion.cmi: nCicUnifHint.cmi 
-nRstatus.cmi: nCicUnifHint.cmi nCicCoercion.cmi 
+nRstatus.cmi: nCicCoercion.cmi 
 nCicUnification.cmi: nRstatus.cmi 
 nCicRefiner.cmi: nRstatus.cmi 
 nDiscriminationTree.cmo: nDiscriminationTree.cmi 
@@ -15,8 +15,8 @@ nCicCoercion.cmo: nDiscriminationTree.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \
     nCicCoercion.cmi 
 nCicCoercion.cmx: nDiscriminationTree.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \
     nCicCoercion.cmi 
-nRstatus.cmo: nCicUnifHint.cmi nCicCoercion.cmi nRstatus.cmi 
-nRstatus.cmx: nCicUnifHint.cmx nCicCoercion.cmx nRstatus.cmi 
+nRstatus.cmo: nCicCoercion.cmi nRstatus.cmi 
+nRstatus.cmx: nCicCoercion.cmx nRstatus.cmi 
 nCicUnification.cmo: nRstatus.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \
     nCicCoercion.cmi nCicUnification.cmi 
 nCicUnification.cmx: nRstatus.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \
diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index f544d8dae..4cb188170 100644
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -53,15 +53,15 @@ let logger =
 
 let mk_type n = 
   if n = 0 then
-     [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
+     [`Type, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
   else
-     [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+     [`Type, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 let mk_cprop n = 
   if n = 0 then 
-    [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
+    [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
   else
-    [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
+    [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 
 
@@ -151,16 +151,9 @@ let _ =
     try
     let rec aux = function
       | a::(b::_ as tl) ->
-         NCicEnvironment.add_constraint true (mk_type a) (mk_type b);
-         NCicEnvironment.add_constraint true (mk_cprop a) (mk_cprop b);
-         NCicEnvironment.add_constraint true (mk_cprop a) (mk_type b);
-         NCicEnvironment.add_constraint true (mk_type a) (mk_cprop b);
-         NCicEnvironment.add_constraint false (mk_cprop a) (mk_type a);
-         NCicEnvironment.add_constraint false (mk_type a) (mk_cprop a);
+         NCicEnvironment.add_lt_constraint (mk_type a) (mk_type b);
+         NCicEnvironment.add_lt_constraint (mk_cprop a) (mk_cprop b);
          aux tl
-      | [a] -> 
-         NCicEnvironment.add_constraint false (mk_type a) (mk_cprop a);
-         NCicEnvironment.add_constraint false (mk_cprop a) (mk_type a);
       | _ -> ()
     in
        aux lll
diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 8dc94e9e4..a1ce81470 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -145,11 +145,12 @@ let rec typeof rdb
            raise (RefineFailure (lazy (localise t,"unbound variable"))))
         in
         metasenv, subst, t, infty
-    | C.Sort (C.Type [false,u]) -> metasenv,subst,t,(C.Sort (C.Type [true, u]))
-    | C.Sort (C.Type _) -> 
-        raise (AssertFailure (lazy ("Cannot type an inferred type: "^
-          NCicPp.ppterm ~subst ~metasenv ~context t)))
-    | C.Sort _ -> metasenv,subst,t,(C.Sort (C.Type NCicEnvironment.type0))
+    | C.Sort s -> 
+         (try metasenv, subst, t, C.Sort (NCicEnvironment.typeof_sort s)
+         with 
+         | NCicEnvironment.UntypableSort msg -> 
+              raise (RefineFailure (lazy (localise t, Lazy.force msg)))
+         | NCicEnvironment.AssertFailure msg -> raise (AssertFailure msg))
     | C.Implicit infos -> 
          let metasenv,_,t,ty =
            exp_implicit ~localise metasenv context expty t infos
@@ -238,7 +239,7 @@ let rec typeof rdb
          | None -> metasenv, subst, None 
          | Some x -> 
              let m, s, x = 
-               NCicUnification.delift_term_wrt_terms 
+               NCicUnification.delift_type_wrt_terms 
                  rdb metasenv subst context x [t]
              in
                m, s, Some x
diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 2f6332d51..dff242970 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -98,11 +98,13 @@ let pp s =
 
 let pp _ = ();;
 
-let ppcontext = NCicPp.ppcontext;;
-let ppmetasenv = NCicPp.ppmetasenv;;
+let ppcontext ~metasenv ~subst c = 
+      "\nctx:\n"^ NCicPp.ppcontext ~metasenv ~subst c
+;;
+let ppmetasenv ~subst m = "\nmenv:\n" ^ NCicPp.ppmetasenv ~subst m;;
 
-let ppcontext ~metasenv:_metasenv ~subst:_subst _context = "...";;
-let ppmetasenv ~subst:_subst _metasenv = "...";;
+let ppcontext ~metasenv:_metasenv ~subst:_subst _context = "";;
+let ppmetasenv ~subst:_subst _metasenv = "";;
 
 let fix_sorts swap exc t =
   let rec aux () = function
@@ -153,7 +155,8 @@ let rec lambda_intros rdb metasenv subst context t args =
        metasenv, subst, bo
    | (arg,ty)::tail ->
        let metasenv, subst, telescopic_ty = 
-         delift_term_wrt_terms rdb metasenv subst context_of_args ty 
+(* XXX         if processed_args = [] then metasenv, subst, ty else  *)
+         delift_type_wrt_terms rdb metasenv subst context_of_args ty 
            (List.rev processed_args)
        in
        let name = "HBeta"^string_of_int n in
@@ -163,7 +166,8 @@ let rec lambda_intros rdb metasenv subst context t args =
        in
         metasenv, subst, NCic.Lambda (name, telescopic_ty, bo)
  in
-   mk_lambda metasenv subst context 0 [] argsty
+ let rc = mk_lambda metasenv subst context 0 [] argsty in
+ rc
 
 and instantiate rdb test_eq_only metasenv subst context n lc t swap =
  (*D*)  inside 'I'; try let rc =  
@@ -181,8 +185,8 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
          (* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *)
     | _ ->
        pp (lazy (
-         "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^
-          ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^
+               "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^
+          ppcontext ~metasenv ~subst context ^ 
           ppmetasenv ~subst metasenv));
        let exc_to_be = fail_exc metasenv subst context (NCic.Meta (n,lc)) t in
        let t, ty_t = 
@@ -194,8 +198,8 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
            if ft == t then 
              (prerr_endline ( ("ILLTYPED: " ^ 
                 NCicPp.ppterm ~metasenv ~subst ~context t
-            ^ "\nBECAUSE:" ^ Lazy.force msg ^ "\nCONTEXT:\n" ^
-            ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^
+            ^ "\nBECAUSE:" ^ Lazy.force msg ^ 
+            ppcontext ~metasenv ~subst context ^ 
             ppmetasenv ~subst metasenv
             ));
                      assert false)
@@ -251,7 +255,7 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
   in
          pp (lazy(string_of_int n ^ " := 222 = "^
            NCicPp.ppterm ~metasenv ~subst ~context:ctx t
-         ^ "\n" ^ ppmetasenv ~subst metasenv));
+         ^ ppmetasenv ~subst metasenv));
   (* Unifying the types may have already instantiated n. *)
   try
     let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
@@ -276,7 +280,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
    let fo_unif test_eq_only metasenv subst t1 t2 =
     (*D*) inside 'F'; try let rc =  
      pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ 
-         NCicPp.ppterm ~metasenv ~subst ~context t2 ^ "\n" ^ ppmetasenv
+         NCicPp.ppterm ~metasenv ~subst ~context t2 ^ ppmetasenv
          ~subst metasenv));
      if t1 === t2 then
        metasenv, subst
@@ -661,9 +665,9 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
           | Uncertain _ -> raise exn
  (*D*)  in outside(); rc with exn -> outside (); raise exn 
 
-and delift_term_wrt_terms rdb metasenv subst context t args =
+and delift_type_wrt_terms rdb metasenv subst context t args =
   let metasenv, _, instance, _ =
-    NCicMetaSubst.mk_meta metasenv context `Term in
+    NCicMetaSubst.mk_meta metasenv context `Type in
   let meta_applied = NCicUntrusted.mk_appl instance args in
   let metasenv,subst,meta_applied,_ =
     !refiner_typeof ((rdb:> NRstatus.status)#set_coerc_db NCicCoercion.empty_db)
@@ -681,4 +685,4 @@ let unify rdb ?(test_eq_only=false) =
   indent := "";      
   unify rdb test_eq_only;;
 
-let fix_sorts = fix_sorts false (UnificationFailure (lazy "no sup"));;
+let fix_sorts = fix_sorts true (UnificationFailure (lazy "no sup"));;
diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli
index 944b4c187..c442306d7 100644
--- a/helm/software/components/ng_refiner/nCicUnification.mli
+++ b/helm/software/components/ng_refiner/nCicUnification.mli
@@ -32,7 +32,7 @@ val unify :
 (* this should be moved elsewhere *)
 val fix_sorts: NCic.term -> NCic.term
 
-val delift_term_wrt_terms:
+val delift_type_wrt_terms:
   #NRstatus.status -> 
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
   NCic.term -> NCic.term list ->
diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend
index 636e38f58..7c97b8cfa 100644
--- a/helm/software/components/ng_tactics/.depend
+++ b/helm/software/components/ng_tactics/.depend
@@ -1,12 +1,12 @@
 nCicTacReduction.cmi: 
 nTacStatus.cmi: 
-nTactics.cmi: nTacStatus.cmi 
 nCicElim.cmi: 
+nTactics.cmi: nTacStatus.cmi 
 nCicTacReduction.cmo: nCicTacReduction.cmi 
 nCicTacReduction.cmx: nCicTacReduction.cmi 
 nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi 
 nTacStatus.cmx: nCicTacReduction.cmx nTacStatus.cmi 
-nTactics.cmo: nTacStatus.cmi nTactics.cmi 
-nTactics.cmx: nTacStatus.cmx nTactics.cmi 
 nCicElim.cmo: nCicElim.cmi 
 nCicElim.cmx: nCicElim.cmi 
+nTactics.cmo: nTacStatus.cmi nCicElim.cmi nTactics.cmi 
+nTactics.cmx: nTacStatus.cmx nCicElim.cmx nTactics.cmi 
diff --git a/helm/software/components/ng_tactics/.depend.opt b/helm/software/components/ng_tactics/.depend.opt
index 636e38f58..7c97b8cfa 100644
--- a/helm/software/components/ng_tactics/.depend.opt
+++ b/helm/software/components/ng_tactics/.depend.opt
@@ -1,12 +1,12 @@
 nCicTacReduction.cmi: 
 nTacStatus.cmi: 
-nTactics.cmi: nTacStatus.cmi 
 nCicElim.cmi: 
+nTactics.cmi: nTacStatus.cmi 
 nCicTacReduction.cmo: nCicTacReduction.cmi 
 nCicTacReduction.cmx: nCicTacReduction.cmi 
 nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi 
 nTacStatus.cmx: nCicTacReduction.cmx nTacStatus.cmi 
-nTactics.cmo: nTacStatus.cmi nTactics.cmi 
-nTactics.cmx: nTacStatus.cmx nTactics.cmi 
 nCicElim.cmo: nCicElim.cmi 
 nCicElim.cmx: nCicElim.cmi 
+nTactics.cmo: nTacStatus.cmi nCicElim.cmi nTactics.cmi 
+nTactics.cmx: nTacStatus.cmx nCicElim.cmx nTactics.cmi 
diff --git a/helm/software/components/ng_tactics/Makefile b/helm/software/components/ng_tactics/Makefile
index 139f27288..e5a613439 100644
--- a/helm/software/components/ng_tactics/Makefile
+++ b/helm/software/components/ng_tactics/Makefile
@@ -3,8 +3,8 @@ PACKAGE = ng_tactics
 INTERFACE_FILES = \
 	nCicTacReduction.mli \
 	nTacStatus.mli \
-	nTactics.mli \
-	nCicElim.mli
+	nCicElim.mli \
+	nTactics.mli 
 
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 
diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index d5cbca892..4117c4ffa 100644
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -154,19 +154,24 @@ let mk_elim uri leftno it (outsort,suffix) =
 ;;
 
 let ast_of_sort s =
+  let headrm prefix s =
+    try 
+      let len_prefix = String.length prefix in 
+      assert (String.sub s 0 len_prefix = prefix);
+      String.sub s len_prefix (String.length s - len_prefix)
+    with Invalid_argument _ -> assert false
+  in
   match s with
-     NCic.Prop -> `Prop,"ind"
-   | NCic.Type u ->
-      let u = NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] (NCic.Sort s) in
-      (try
-        if String.sub u 0 4 = "Type" then
-         `NType (String.sub u 4 (String.length u - 4)), "rect_" ^ u
-        else if String.sub u 0 5 = "CProp" then
-         `NCProp (String.sub u 5 (String.length u - 5)), "rect_" ^ u
-        else
-         (prerr_endline u;
-         assert false)
-       with Failure _ -> assert false)
+   | NCic.Prop -> `Prop,"ind"
+   | NCic.Type []  -> `NType "", "rect_Type"
+   | NCic.Type ((`Type,u) :: _) ->
+       let name = NUri.name_of_uri u in
+       `NType (headrm "Type" name), "rect_" ^ name
+   | NCic.Type ((`CProp,u) :: _) ->
+       let name = NUri.name_of_uri u in
+       `NCProp (headrm "Type" name), 
+       "rect_" ^ Str.replace_first (Str.regexp "Type") "CProp" name
+   | _ -> assert false
 ;;
 
 let mk_elims (uri,_,_,_,obj) =
diff --git a/helm/software/components/ng_tactics/nCicElim.mli b/helm/software/components/ng_tactics/nCicElim.mli
index e8b4c7a8d..bbb96facb 100644
--- a/helm/software/components/ng_tactics/nCicElim.mli
+++ b/helm/software/components/ng_tactics/nCicElim.mli
@@ -13,3 +13,5 @@
 
 val mk_elims: NCic.obj -> CicNotationPt.term CicNotationPt.obj list
 val mk_projections: NCic.obj -> CicNotationPt.term CicNotationPt.obj list
+val ast_of_sort : 
+  NCic.sort -> [> `NCProp of string | `NType of string | `Prop ]  * string
diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index 25beed259..0bb0d846e 100644
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -14,7 +14,7 @@
 exception Error of string lazy_t * exn option
 let fail ?exn msg = raise (Error (msg,exn))
 
-let wrap f x = 
+let wrap f x =
   try f x 
   with 
   | MultiPassDisambiguator.DisambiguationError _ 
diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 0ba8e4b44..01a57f0c4 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -477,33 +477,31 @@ let analyze_indty_tac ~what indtyref =
   exec id_tac status goal)
 ;;
 
+let sort_of_goal_tac sortref = distribute_tac (fun status goal ->
+  let goalty = get_goalty status goal in
+  let status,sort = typeof status (ctx_of goalty) goalty in
+  let sort = fix_sorts sort in
+  let status, sort = term_of_cic_term status sort (ctx_of goalty) in
+   sortref := sort;
+   status)
+;;
+
 let elim_tac ~what:(txt,len,what) ~where = 
   let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
   let indtyinfo = ref None in
-  let sort = ref None in
-  let compute_goal_sort_tac = distribute_tac (fun status goal ->
-    let goalty = get_goalty status goal in
-    let status, goalsort = typeof status (ctx_of goalty) goalty in
-    let goalsort = fix_sorts goalsort in
-    sort := Some goalsort;
-    exec id_tac status goal)
-  in
+  let sort = ref (NCic.Rel 1) in
   atomic_tac (block_tac [
     analyze_indty_tac ~what indtyinfo;    
     (fun s -> select_tac 
       ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s);
-    compute_goal_sort_tac;
+    sort_of_goal_tac sort;
     (fun status ->
-     let sort = HExtlib.unopt !sort in
      let ity = HExtlib.unopt !indtyinfo in
      let NReference.Ref (uri, _) = ity.reference in
-     let status, sort = term_of_cic_term status sort (ctx_of sort) in
-     let name = NUri.name_of_uri uri ^
-      match sort with
-       | NCic.Sort NCic.Prop -> "_ind"
-       | NCic.Sort NCic.Type u ->
-          "_rect_" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] sort
-       | _ -> assert false 
+     let name = 
+       NUri.name_of_uri uri ^ "_" ^
+        snd (NCicElim.ast_of_sort 
+          (match !sort with NCic.Sort x -> x | _ -> assert false))
      in
      let eliminator = 
        let _,_,w = what in
@@ -512,23 +510,11 @@ let elim_tac ~what:(txt,len,what) ~where =
      exact_tac ("",0,eliminator) status) ]) 
 ;;
 
-let sort_of_goal_tac sortref = distribute_tac (fun status goal ->
-  let goalty = get_goalty status goal in
-  let status,sort = typeof status (ctx_of goalty) goalty in
-  let status,sort = term_of_cic_term status sort (ctx_of goalty) in
-   sortref := sort;
-   status)
-;;
-
 let rewrite_tac ~dir ~what:(_,_,what) ~where status =
  let sortref = ref (NCic.Rel 1) in
  let status = sort_of_goal_tac sortref status in
- let suffix =
-  match !sortref with
-   | NCic.Sort NCic.Prop -> "_ind"
-   | NCic.Sort NCic.Type u ->
-      "_rect_" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] !sortref
-   | _ -> assert false 
+ let suffix = "_" ^ snd (NCicElim.ast_of_sort 
+   (match !sortref with NCic.Sort x -> x | _ -> assert false))
  in
  let name =
   match dir with
diff --git a/helm/software/matita/contribs/formal_topology/overlap/depends b/helm/software/matita/contribs/formal_topology/overlap/depends
index c6d981528..b67a2e7c1 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/depends
+++ b/helm/software/matita/contribs/formal_topology/overlap/depends
@@ -1,26 +1,26 @@
-o-basic_pairs.ma notation.ma o-algebra.ma
 basic_pairs_to_basic_topologies.ma basic_pairs.ma basic_pairs_to_o-basic_pairs.ma basic_topologies.ma o-basic_pairs_to_o-basic_topologies.ma
-o-saturations.ma o-algebra.ma
-saturations.ma relations.ma
+o-basic_pairs.ma notation.ma o-algebra.ma
 o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma
 basic_pairs.ma notation.ma relations.ma
-formal_topologies.ma basic_topologies.ma
+saturations.ma relations.ma
+o-saturations.ma o-algebra.ma
 o-algebra.ma categories.ma
 categories.ma cprop_connectives.ma
+formal_topologies.ma basic_topologies.ma
 o-formal_topologies.ma o-basic_topologies.ma
 saturations_to_o-saturations.ma o-saturations.ma relations_to_o-algebra.ma saturations.ma
-subsets.ma categories.ma
 basic_topologies.ma relations.ma saturations.ma
 concrete_spaces.ma basic_pairs.ma
-r-o-basic_pairs.ma apply_functor.ma basic_pairs_to_o-basic_pairs.ma
+subsets.ma categories.ma
 relations.ma subsets.ma
+r-o-basic_pairs.ma apply_functor.ma basic_pairs_to_o-basic_pairs.ma o-basic_pairs_to_o-basic_topologies.ma
 concrete_spaces_to_o-concrete_spaces.ma basic_pairs_to_o-basic_pairs.ma concrete_spaces.ma o-concrete_spaces.ma
 o-basic_topologies.ma o-algebra.ma o-saturations.ma
 notation.ma 
 basic_topologies_to_o-basic_topologies.ma basic_topologies.ma o-basic_topologies.ma relations_to_o-algebra.ma
 basic_pairs_to_o-basic_pairs.ma basic_pairs.ma o-basic_pairs.ma relations_to_o-algebra.ma
-apply_functor.ma categories.ma
+apply_functor.ma categories.ma notation.ma
 cprop_connectives.ma logic/connectives.ma
-relations_to_o-algebra.ma o-algebra.ma relations.ma
 o-basic_pairs_to_o-basic_topologies.ma notation.ma o-basic_pairs.ma o-basic_topologies.ma
+relations_to_o-algebra.ma o-algebra.ma relations.ma
 logic/connectives.ma 
diff --git a/helm/software/matita/nlibrary/logic/connectives.ma b/helm/software/matita/nlibrary/logic/connectives.ma
index a149bc9dd..34661dc80 100644
--- a/helm/software/matita/nlibrary/logic/connectives.ma
+++ b/helm/software/matita/nlibrary/logic/connectives.ma
@@ -14,38 +14,38 @@
 
 include "logic/pts.ma".
 
-ninductive True: CProp ≝
+ninductive True: CProp[0] ≝
   I : True.
 
-ninductive False: CProp ≝.
+ninductive False: CProp[0] ≝.
 
-ndefinition Not: CProp → CProp ≝
+ndefinition Not: CProp[0] → CProp[0] ≝
   λA. A → False.
 
 interpretation "logical not" 'not x = (Not x).
 
-ninductive And (A,B:CProp) : CProp ≝
+ninductive And (A,B:CProp[0]) : CProp[0] ≝
     conj : A → B → And A B.
 
 interpretation "logical and" 'and x y = (And x y).
 
-ninductive Or (A,B:CProp) : CProp ≝
+ninductive Or (A,B:CProp[0]) : CProp[0] ≝
      or_introl : A → Or A B
    | or_intror : B → Or A B.
 
 interpretation "logical or" 'or x y = (Or x y).
 
-ninductive Ex (A:Type) (P:A → CProp) : CProp ≝
+ninductive Ex (A:Type[0]) (P:A → CProp[0]) : CProp[0] ≝
     ex_intro: ∀x:A. P x → Ex A P.
 
 
-ninductive Ex1 (A:Type[1]) (P:A → CProp) : CProp[1] ≝
+ninductive Ex1 (A:Type[1]) (P:A → CProp[0]) : CProp[1] ≝
     ex_intro1: ∀x:A. P x → Ex1 A P.
 
 interpretation "exists1" 'exists x = (Ex1 ? x).
 interpretation "exists" 'exists x = (Ex ? x).
 
-nrecord iff (A,B: CProp) : CProp ≝
+nrecord iff (A,B: CProp[0]) : CProp[0] ≝
  { if: A → B;
    fi: B → A
  }.
diff --git a/helm/software/matita/nlibrary/logic/pts.ma b/helm/software/matita/nlibrary/logic/pts.ma
index d895b59e7..e4f0815ff 100644
--- a/helm/software/matita/nlibrary/logic/pts.ma
+++ b/helm/software/matita/nlibrary/logic/pts.ma
@@ -12,17 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-universe constraint Type[0] ≤ CProp[0].
-universe constraint CProp[0] ≤ Type[0].
-
-universe constraint Type[1] ≤ CProp[1].
-universe constraint CProp[1] ≤ Type[1].
-
-universe constraint Type[2] ≤ CProp[2].
-universe constraint CProp[2] ≤ Type[2].
-
 universe constraint Type[0] < Type[1].
-universe constraint CProp[0] < CProp[1].
-
 universe constraint Type[1] < Type[2].
-universe constraint CProp[1] < CProp[2].
\ No newline at end of file
+
diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index 7affc517f..61173c78e 100644
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -18,24 +18,21 @@ include "nat/compare.ma".
 include "nat/minus.ma".
 include "datatypes/pairs.ma".
 
-alias symbol "eq" (instance 2) = "leibnitz's equality".
-alias symbol "eq" (instance 1) = "setoid eq".
 alias symbol "eq" = "setoid eq".
+
 alias symbol "eq" = "setoid1 eq".
 alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
 alias symbol "eq" = "setoid eq".
 alias symbol "eq" = "setoid1 eq".
-alias symbol "eq" = "setoid eq".
 nrecord partition (A: setoid) : Type[1] ≝ 
  { support: setoid;
    indexes: qpowerclass support;
    class: unary_morphism1 (setoid1_of_setoid support) (qpowerclass_setoid A);
    inhabited: ∀i. i ∈ indexes → class i ≬ class i;
-   disjoint: ∀i,j. i ∈ indexes → j ∈ indexes → class i ≬ class j → i=j;
-   covers: big_union support ? ? (λx.class x) = full_set A
- }. napply indexes; nqed.
-
+   disjoint: ∀i,j. i ∈ indexes → j ∈ indexes → class i ≬ class j → i = j;
+   covers: big_union support ? indexes (λx.class x) = full_set A
+ }.
+ 
 naxiom daemon: False.
 
 nlet rec iso_nat_nat_union (s: nat → nat) m index on index : pair nat nat ≝
@@ -153,7 +150,9 @@ nlemma partition_splits_card:
     ngeneralize in match (Hc y I) in ⊢ ?; *; #index; *; #Hi1; #Hi2;
     ngeneralize in match (f_sur ???? f ? Hi1) in ⊢ ?; *; #nindex; *; #Hni1; #Hni2;
     ngeneralize in match (f_sur ???? (fi nindex) y ?) in ⊢ ?
-     [##2: napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
+     [##2: alias symbol "refl" = "refl".
+alias symbol "prop1" = "prop11".
+napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
     *; #nindex2; *; #Hni21; #Hni22;
     nletin xxx ≝ (plus (big_plus (minus n nindex) (λi.λ_.s (S (plus i nindex)))) nindex2);
     napply (ex_intro … xxx); napply conj
diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index c8a19354c..4e7418fd9 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -228,9 +228,31 @@ nlemma first_omomorphism_theorem_functions3:
  #A; #B; #f; nwhd; #x; #x'; #Hx; #Hx'; #K; nassumption.
 nqed.
 
-nrecord isomorphism (A) (B) (S: qpowerclass A) (T: qpowerclass B) : CProp[0] ≝
+nrecord isomorphism (A, B : setoid) (S: qpowerclass A) (T: qpowerclass B) : Type[0] ≝
  { iso_f:> unary_morphism A B;
    f_closed: ∀x. x ∈ S → iso_f x ∈ T;
    f_sur: surjective … S T iso_f;
    f_inj: injective … S iso_f
  }.
+
+(*
+nrecord isomorphism (A, B : setoid) (S: qpowerclass A) (T: qpowerclass B) : CProp[0] ≝
+ { iso_f:> unary_morphism A B;
+   f_closed: ∀x. x ∈ pc A S → fun1 ?? iso_f x ∈ pc B T}.
+   
+   
+ncheck (λA:?.
+   λB:?.
+    λS:?.
+     λT:?.
+      λxxx:isomorphism A B S T.
+       match xxx
+       return λxxx:isomorphism A B S T.
+               ∀x: carr A.
+                ∀x_72: mem (carr A) (pc A S) x.
+                 mem (carr B) (pc B T) (fun1 A B ((λ_.?) A B S T xxx) x)
+        with [ mk_isomorphism _ yyy ⇒ yyy ] ).   
+   
+   ;
+ }.
+*)