ensembles de contraintes d'univers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@78 85f007b7-540e-0410-9357-904b9bb8a0f7

16 files changed, 300 insertions, 264 deletions

diff --git a/kernel/constant.ml b/kernel/constant.ml
index ba932b788..39eda93fc 100644
--- a/kernel/constant.ml
+++ b/kernel/constant.ml
@@ -2,6 +2,7 @@
 (* $Id$ *)
 
 open Names
+open Univ
 open Generic
 open Term
 open Sign
@@ -25,6 +26,7 @@ type constant_body = {
   const_body : recipe ref option;
   const_type : typed_type;
   const_hyps : typed_type signature;
+  const_constraints : constraints;
   mutable const_opaque : bool }
 
 let is_defined cb = 
diff --git a/kernel/constant.mli b/kernel/constant.mli
index 890e1f425..d9adc6d75 100644
--- a/kernel/constant.mli
+++ b/kernel/constant.mli
@@ -3,6 +3,7 @@
 
 (*i*)
 open Names
+open Univ
 open Term
 open Sign
 (*i*)
@@ -20,6 +21,7 @@ type constant_body = {
   const_body : recipe ref option;
   const_type : typed_type;
   const_hyps : typed_type signature;
+  const_constraints : constraints;
   mutable const_opaque : bool }
 
 val is_defined : constant_body -> bool
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4306f3ae4..a97c92a5d 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -61,6 +61,12 @@ let push_rel idrel env =
 let set_universes g env =
   if env.env_universes == g then env else { env with env_universes = g }
 
+let add_constraints c env =
+  if c == Constraint.empty then 
+    env 
+  else 
+    { env with env_universes = merge_constraints c env.env_universes }
+
 let add_constant sp cb env =
   let new_constants = Spmap.add sp cb env.env_globals.env_constants in
   let new_locals = (Constant,sp)::env.env_globals.env_locals in
@@ -297,7 +303,14 @@ let import cenv env =
       env_locals = gl.env_locals;
       env_imports = (cenv.cenv_id,cenv.cenv_stamp) :: gl.env_imports }
   in
-  { env with env_globals = new_globals }
+  let g = universes env in
+  let g = List.fold_left 
+	    (fun g (_,cb) -> merge_constraints cb.const_constraints g) 
+	    g cenv.cenv_constants in
+  let g = List.fold_left 
+	    (fun g (_,mib) -> merge_constraints mib.mind_constraints g) 
+	    g cenv.cenv_inductives in
+  { env with env_globals = new_globals; env_universes = g }
 
 (*s Judgments. *)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 3e88fcfd1..4d979f0dc 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -29,6 +29,7 @@ val context : 'a unsafe_env -> context
 val push_var : identifier * typed_type -> 'a unsafe_env -> 'a unsafe_env
 val push_rel : name * typed_type -> 'a unsafe_env -> 'a unsafe_env
 val set_universes : universes -> 'a unsafe_env -> 'a unsafe_env
+val add_constraints : constraints -> 'a unsafe_env -> 'a unsafe_env
 val add_constant : 
   section_path -> constant_body -> 'a unsafe_env -> 'a unsafe_env
 val add_mind : 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 0988ae197..b6a7c0a3e 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -222,7 +222,7 @@ let is_recursive listind =
   in 
   array_exists one_is_rec
 
-let cci_inductive env env_ar kind nparams finite inds =
+let cci_inductive env env_ar kind nparams finite inds cst =
   let ntypes = List.length inds in
   let one_packet i (id,ar,cnames,issmall,isunit,lc) =
     let recargs = listrec_mconstr env_ar ntypes nparams i lc in
@@ -241,5 +241,6 @@ let cci_inductive env env_ar kind nparams finite inds =
     mind_ntypes = ntypes;
     mind_hyps = get_globals (context env);
     mind_packets = packets;
+    mind_constraints = cst;
     mind_singl = None;
     mind_nparams = nparams }
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index ebb1e1f67..8a200aab0 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -3,6 +3,7 @@
 
 (*i*)
 open Names
+open Univ
 open Term
 open Inductive
 open Environ
@@ -18,5 +19,5 @@ val sort_of_arity : 'a unsafe_env -> constr -> sorts
 val cci_inductive : 
   'a unsafe_env -> 'a unsafe_env -> path_kind -> int -> bool -> 
     (identifier * typed_type * identifier list * bool * bool * constr) list ->
-      mutual_inductive_body
-
+      constraints ->
+      	mutual_inductive_body
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 5617358a1..4034d9712 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -3,6 +3,7 @@
 
 open Util
 open Names
+open Univ
 open Generic
 open Term
 open Sign
@@ -27,6 +28,7 @@ type mutual_inductive_body = {
   mind_ntypes : int;
   mind_hyps : typed_type signature;
   mind_packets : mutual_inductive_packet array;
+  mind_constraints : constraints;
   mind_singl : constr option;
   mind_nparams : int }
 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index d0dee30b9..cd23920cf 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -3,6 +3,7 @@
 
 (*i*)
 open Names
+open Univ
 open Term
 open Sign
 (*i*)
@@ -29,6 +30,7 @@ type mutual_inductive_body = {
   mind_ntypes : int;
   mind_hyps : typed_type signature;
   mind_packets : mutual_inductive_packet array;
+  mind_constraints : constraints;
   mind_singl : constr option;
   mind_nparams : int }
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index f16fa0d8c..2d19f4485 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -742,42 +742,27 @@ let pb_equal = function
   | CONV_LEQ -> CONV
   | CONV -> CONV
 
-type conversion_result =
-  | Convertible of universes
-  | NotConvertible
-
-type 'a conversion_function = 
-    'a unsafe_env -> constr -> constr -> conversion_result
+type 'a conversion_function = 'a unsafe_env -> constr -> constr -> constraints
 
 (* Conversion utility functions *)
 
-let convert_of_constraint f u =
-  try Convertible (f u) with UniverseInconsistency -> NotConvertible
+type conversion_test = constraints -> constraints
 
-type conversion_test = universes -> conversion_result
+exception NotConvertible
 
-let convert_of_bool b u =
-  if b then Convertible u else NotConvertible
+let convert_of_bool b c =
+  if b then c else raise NotConvertible
 
 let bool_and_convert b f = 
-  if b then f else fun _ -> NotConvertible
+  if b then f else fun _ -> raise NotConvertible
 
-let convert_and f1 f2 u = 
-  match f1 u with
-    | Convertible u' -> f2 u'
-    | NotConvertible -> NotConvertible
+let convert_and f1 f2 c = f2 (f1 c)
 
-let convert_or f1 f2 u =
-  match f1 u with
-    | NotConvertible -> f2 u
-    | c -> c
+let convert_or f1 f2 c =
+  try f1 c with NotConvertible -> f2 c
 
-let convert_forall2 f v1 v2 u =
-  array_fold_left2 
-    (fun a x y -> match a with
-       | NotConvertible -> NotConvertible
-       | Convertible u -> f x y u)
-    (Convertible u) v1 v2
+let convert_forall2 f v1 v2 c =
+  array_fold_left2 (fun c x y -> f x y c) c v1 v2
 
 (* Convertibility of sorts *)
 
@@ -787,9 +772,9 @@ let sort_cmp pb s0 s1 =
     | (Prop c1, Type u)  -> convert_of_bool (not (pb_is_equal pb))
     | (Type u1, Type u2) ->
 	(match pb with
-           | CONV -> convert_of_constraint (enforce_eq u1 u2)
-	   | CONV_LEQ -> convert_of_constraint (enforce_geq u2 u1))
-    | (_, _) -> fun _ -> NotConvertible
+           | CONV -> enforce_eq u1 u2
+	   | CONV_LEQ -> enforce_geq u2 u1)
+    | (_, _) -> fun _ -> raise NotConvertible
 
 let base_sort_cmp pb s0 s1 =
   match (s0,s1) with
@@ -845,7 +830,7 @@ and eqappr cv_pb infos appr1 appr2 =
              | None -> (match search_frozen_cst infos (Const sp1) al1 with
                           | Some def1 -> eqappr cv_pb infos
 				(lft1, fhnf_apply infos n1 def1 v1) appr2
-			  | None -> fun _ -> NotConvertible))
+			  | None -> fun _ -> raise NotConvertible))
 
     | (FOPN(Abst sp1,al1), FOPN(Abst sp2,al2)) ->
 	convert_or
@@ -861,20 +846,20 @@ and eqappr cv_pb infos appr1 appr2 =
              | None -> (match search_frozen_cst infos (Abst sp1) al2 with
                           | Some def1 -> eqappr cv_pb infos
 				(lft1, fhnf_apply infos n1 def1 v1) appr2
-			  | None -> fun _ -> NotConvertible))
+			  | None -> fun _ -> raise NotConvertible))
 
     (* only one constant or abstraction *)
     | (FOPN((Const _ | Abst _) as op,al1), _)      ->
         (match search_frozen_cst infos op al1 with
            | Some def1 -> 
 	       eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1) appr2
-           | None -> fun _ -> NotConvertible)
+           | None -> fun _ -> raise NotConvertible)
 
     | (_, FOPN((Const _ | Abst _) as op,al2))      ->
         (match search_frozen_cst infos op al2 with
            | Some def2 -> 
 	       eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2)
-           | None -> fun _ -> NotConvertible)
+           | None -> fun _ -> raise NotConvertible)
 	
     (* other constructors *)
     | (FOP2(Lambda,c1,c2), FOP2(Lambda,c'1,c'2)) ->
@@ -920,48 +905,35 @@ and eqappr cv_pb infos appr1 appr2 =
            (convert_forall2 
 	      (ccnv cv_pb infos (el_lift el1) (el_lift el2)) vc1 vc2)
 
-     | _ -> (fun _ -> NotConvertible)
+     | _ -> (fun _ -> raise NotConvertible)
 
 
 let fconv cv_pb env t1 t2 =
   let t1 = strong (fun _ -> strip_outer_cast) env t1
   and t2 = strong (fun _ -> strip_outer_cast) env t2 in
-  let univ = universes env in
   if eq_constr t1 t2 then 
-    Convertible univ
+    Constraint.empty
   else
     let infos = create_clos_infos hnf_flags env in
-    ccnv cv_pb infos ELID ELID (inject t1) (inject t2) univ
+    ccnv cv_pb infos ELID ELID (inject t1) (inject t2) Constraint.empty
 
-let conv env term1 term2 = fconv CONV env term1 term2
-let conv_leq env term1 term2 = fconv CONV_LEQ env term1 term2
+let conv env = fconv CONV env
+let conv_leq env = fconv CONV_LEQ env 
 
 let conv_forall2 f env v1 v2 =
-  let (_,c) =
-    array_fold_left2 
-      (fun a x y -> match a with
-	 | (_,NotConvertible) -> a
-	 | (e,Convertible u) -> let e' = set_universes u env in (e',f e x y))
-      (env, Convertible (universes env)) 
-      v1 v2
-  in
-  c
+  array_fold_left2 
+    (fun c x y -> let c' = f env x y in Constraint.union c c')
+    Constraint.empty
+    v1 v2
 
 let conv_forall2_i f env v1 v2 =
-  let (_,c) =
-    array_fold_left2_i 
-      (fun i a x y -> match a with
-	 | (_,NotConvertible) -> a
-	 | (e,Convertible u) -> let e' = set_universes u env in (e',f i e x y))
-      (env, Convertible (universes env)) 
-      v1 v2
-  in
-  c
+  array_fold_left2_i 
+    (fun i c x y -> let c' = f i env x y in Constraint.union c c')
+    Constraint.empty
+    v1 v2
 
 let test_conversion f env x y =
-  match f env x y with
-    | Convertible _ -> true
-    | NotConvertible -> false
+  try let _ = f env x y in true with NotConvertible -> false
 
 let is_conv env = test_conversion conv env
 let is_conv_leq env = test_conversion conv_leq env
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 6e6c243c7..8b2d988c3 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -129,11 +129,9 @@ type conv_pb =
 val pb_is_equal : conv_pb -> bool
 val pb_equal : conv_pb -> conv_pb
 
-type conversion_result =
-  | Convertible of universes
-  | NotConvertible
+type conversion_test = constraints -> constraints
 
-type conversion_test = universes -> conversion_result
+exception NotConvertible
 
 val sort_cmp : conv_pb -> sorts -> sorts -> conversion_test
 val base_sort_cmp : conv_pb -> sorts -> sorts -> bool
@@ -144,28 +142,23 @@ val convert_or : conversion_test -> conversion_test -> conversion_test
 val convert_forall2 : 
   ('a -> 'b -> conversion_test) -> 'a array -> 'b array -> conversion_test
 
-type 'a conversion_function = 
-    'a unsafe_env -> constr -> constr -> conversion_result
+type 'a conversion_function = 'a unsafe_env -> constr -> constr -> constraints
 
 val fconv : conv_pb -> 'a conversion_function
 
-(* [fconv] has 2 instances:
-   \begin{itemize}
-   \item [conv = fconv CONV] : 
-     conversion test, and adjust universes constraints
-   \item [conv_leq = fconv CONV_LEQ] : cumulativity test, adjust universes
-   \end{itemize} *)
+(* [fconv] has 2 instances: [conv = fconv CONV] i.e. conversion test, and
+   [conv_leq = fconv CONV_LEQ] i.e. cumulativity test. *)
 
 val conv : 'a conversion_function
 val conv_leq : 'a conversion_function
 
 val conv_forall2 : 
   'a conversion_function -> 'a unsafe_env 
-    -> constr array -> constr array -> conversion_result
+    -> constr array -> constr array -> constraints
 
 val conv_forall2_i : 
   (int -> 'a conversion_function) -> 'a unsafe_env 
-    -> constr array -> constr array -> conversion_result
+    -> constr array -> constr array -> constraints
 
 val is_conv : 'a unsafe_env -> constr -> constr -> bool
 val is_conv_leq : 'a unsafe_env -> constr -> constr -> bool
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index afc79925f..f863a079f 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -337,41 +337,40 @@ let type_of_prop_or_set cts =
 
 (* Type of Type(i). *)
 
-let type_of_type u g =
-  let (uu,g') = super u g in
-  let (uuu,g'') = super uu g' in
+let type_of_type u =
+  let (uu,uuu,c) = super_super u in
   { uj_val = DOP0 (Sort (Type u));
     uj_type = DOP0 (Sort (Type uu));
     uj_kind = DOP0 (Sort (Type uuu)) },
-  g''
+  c
 
-let type_of_sort c g =
+let type_of_sort c =
   match c with
-    | DOP0 (Sort (Type u)) -> let (uu,g') = super u g in mkType uu, g'
-    | DOP0 (Sort (Prop _)) -> mkType prop_univ, g
+    | DOP0 (Sort (Type u)) -> let (uu,cst) = super u in mkType uu, cst
+    | DOP0 (Sort (Prop _)) -> mkType prop_univ, Constraint.empty
     | _ -> invalid_arg "type_of_sort"
 
 (* Type of a lambda-abstraction. *)
 
-let sort_of_product domsort rangsort g0 =
+let sort_of_product domsort rangsort g =
   match rangsort with
     (* Product rule (s,Prop,Prop) *) 
-    | Prop _ -> rangsort, g0
+    | Prop _ -> rangsort, Constraint.empty
     | Type u2 ->
         (match domsort with
            (* Product rule (Prop,Type_i,Type_i) *)
-           | Prop _ -> rangsort, g0
+           | Prop _ -> rangsort, Constraint.empty
            (* Product rule (Type_i,Type_i,Type_i) *) 
-           | Type u1 -> let (u12,g1) = sup u1 u2 g0 in Type u12, g1)
+           | Type u1 -> let (u12,cst) = sup u1 u2 g in Type u12, cst)
 
 let abs_rel env name var j =
   let rngtyp = whd_betadeltaiota env j.uj_kind in
   let cvar = incast_type var in
-  let (s,g) = sort_of_product var.typ (destSort rngtyp) (universes env) in
+  let (s,cst) = sort_of_product var.typ (destSort rngtyp) (universes env) in
   { uj_val = mkLambda name cvar (j_val j);
     uj_type = mkProd name cvar j.uj_type;
     uj_kind = mkSort s },
-  g
+  cst
 
 (* Type of a product. *)
 
@@ -386,7 +385,7 @@ let gen_rel env name var j =
       | DOP0(Sort s) ->
 	  let (s',g) = sort_of_product var.typ s (universes env) in
           let res_type = mkSort s' in
-	  let (res_kind,g') = type_of_sort res_type g in
+	  let (res_kind,g') = type_of_sort res_type in
           { uj_val = 
 	      mkProd name (mkCast var.body (mkSort var.typ)) (j_val_cast j);
             uj_type = res_type;
@@ -406,29 +405,29 @@ let cast_rel env cj tj =
 
 (* Type of an application. *)
 
-let apply_rel_list env0 nocheck argjl funj =
-  let rec apply_rec env typ = function
+let apply_rel_list env nocheck argjl funj =
+  let rec apply_rec typ cst = function
     | [] -> 
 	{ uj_val  = applist (j_val_only funj, List.map j_val_only argjl);
           uj_type = typ;
           uj_kind = funj.uj_kind },
-	universes env
+	cst
     | hj::restjl ->
         match whd_betadeltaiota env typ with
           | DOP2(Prod,c1,DLAM(_,c2)) ->
               if nocheck then
-                apply_rec env (subst1 hj.uj_val c2) restjl
+                apply_rec (subst1 hj.uj_val c2) cst restjl
 	      else 
-		(match conv_leq env hj.uj_type c1 with
-		   | Convertible g ->
-		       let env' = set_universes g env in
-		       apply_rec env' (subst1 hj.uj_val c2) restjl
-		   | NotConvertible -> 
-		       error_cant_apply CCI env "Type Error" funj argjl)
+		(try 
+		   let c = conv_leq env hj.uj_type c1 in
+		   let cst' = Constraint.union cst c in
+		   apply_rec (subst1 hj.uj_val c2) cst' restjl
+		 with NotConvertible -> 
+		   error_cant_apply CCI env "Type Error" funj argjl)
           | _ ->
               error_cant_apply CCI env "Non-functional construction" funj argjl
   in 
-  apply_rec env0 funj.uj_type argjl
+  apply_rec funj.uj_type Constraint.empty argjl
 
 
 (* Fixpoints. *)
@@ -895,16 +894,10 @@ let type_fixpoint env lna lar vdefj =
   let lt = Array.length vdefj in
   assert (Array.length lar = lt);
   try
-    let cv = 
-      conv_forall2_i
-	(fun i e def ar -> 
-	   let c = conv_leq e def (lift lt ar) in
-	   if c = NotConvertible then raise (IllBranch i) else c)
-	env (Array.map (fun j -> j.uj_type) vdefj) (Array.map body_of_type lar)
-    in
-    begin match cv with
-      | Convertible g -> g
-      | NotConvertible -> assert false
-    end
+    conv_forall2_i
+      (fun i e def ar -> 
+	 try conv_leq e def (lift lt ar) 
+	 with NotConvertible -> raise (IllBranch i))
+      env (Array.map (fun j -> j.uj_type) vdefj) (Array.map body_of_type lar)
   with IllBranch i ->
     error_ill_typed_rec_body CCI env i lna vdefj lar
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index b02e37b1d..992a3a768 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -35,27 +35,25 @@ val type_of_case : 'a unsafe_env -> unsafe_judgment -> unsafe_judgment
 
 val type_of_prop_or_set : contents -> unsafe_judgment
 
-val type_of_type : universe -> universes -> unsafe_judgment * universes
+val type_of_type : universe -> unsafe_judgment * constraints
 
 val abs_rel : 
   'a unsafe_env -> name -> typed_type -> unsafe_judgment 
-    -> unsafe_judgment * universes
+    -> unsafe_judgment * constraints
 
 val gen_rel :
   'a unsafe_env -> name -> typed_type -> unsafe_judgment 
-    -> unsafe_judgment * universes
+    -> unsafe_judgment * constraints
 
 val cast_rel : 
   'a unsafe_env -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment
 
 val apply_rel_list : 
   'a unsafe_env -> bool -> unsafe_judgment list -> unsafe_judgment
-    -> unsafe_judgment * universes
+    -> unsafe_judgment * constraints
 
 val check_fix : 'a unsafe_env -> constr -> unit
 val check_cofix : 'a unsafe_env -> constr -> unit
 
 val type_fixpoint : 'a unsafe_env -> name list -> typed_type array 
-    -> unsafe_judgment array -> universes
-
-
+    -> unsafe_judgment array -> constraints
diff --git a/kernel/typing.ml b/kernel/typing.ml
index 4a029dfe3..dfce2e442 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -38,7 +38,7 @@ type 'a mach_flags = {
 (* The typing machine without information. *)
 
 let rec execute mf env cstr =
-  let u0 = universes env in
+  let cst0 = Constraint.empty in
   match kind_of_term cstr with
     | IsMeta n ->
        	let metaty =
@@ -47,17 +47,17 @@ let rec execute mf env cstr =
 	in
         (match kind_of_term metaty with
            | IsCast (typ,kind) -> 
-	       ({ uj_val = cstr; uj_type = typ; uj_kind = kind }, u0)
+	       ({ uj_val = cstr; uj_type = typ; uj_kind = kind }, cst0)
            | _ ->
-	       let (jty,u1) = execute mf env metaty in
+	       let (jty,cst) = execute mf env metaty in
 	       let k = whd_betadeltaiotaeta env jty.uj_type in
-	       ({ uj_val = cstr; uj_type = metaty; uj_kind = k }, u1))
+	       ({ uj_val = cstr; uj_type = metaty; uj_kind = k }, cst))
 	
     | IsRel n -> 
-	(relative env n, u0)
+	(relative env n, cst0)
 
     | IsVar id -> 
-	(make_judge cstr (snd (lookup_var id env)), u0)
+	(make_judge cstr (snd (lookup_var id env)), cst0)
 	  
     | IsAbst _ ->
         if evaluable_abst env cstr then 
@@ -66,93 +66,91 @@ let rec execute mf env cstr =
 	  error "Cannot typecheck an unevaluable abstraction"
 	      
     | IsConst _ ->
-        (make_judge cstr (type_of_constant_or_existential env cstr), u0)
+        (make_judge cstr (type_of_constant_or_existential env cstr), cst0)
 	  
     | IsMutInd _ ->
-	(make_judge cstr (type_of_inductive env cstr), u0)
+	(make_judge cstr (type_of_inductive env cstr), cst0)
 	  
     | IsMutConstruct _ -> 
 	let (typ,kind) = destCast (type_of_constructor env cstr) in
-        ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , u0)
+        ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , cst0)
 	  
     | IsMutCase (_,p,c,lf) ->
-        let (cj,u1) = execute mf env c in
-	let env1 = set_universes u1 env in
-        let (pj,u2) = execute mf env1 p in
-	let env2 = set_universes u2 env1 in
-        let (lfj,u3) = execute_array mf env2 lf in
-	let env3 = set_universes u3 env2 in
-        (type_of_case env3 pj cj lfj, u3)
+        let (cj,cst1) = execute mf env c in
+        let (pj,cst2) = execute mf env p in
+        let (lfj,cst3) = execute_array mf env lf in
+	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
+        (type_of_case env pj cj lfj, cst)
   
     | IsFix (vn,i,lar,lfi,vdef) ->
         if (not mf.fix) && array_exists (fun n -> n < 0) vn then
           error "General Fixpoints not allowed";
-        let (larv,vdefv,u1) = execute_fix mf env lar lfi vdef in
+        let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in
         let fix = mkFix vn i larv lfi vdefv in
         check_fix env fix;
-	(make_judge fix larv.(i), u1)
+	(make_judge fix larv.(i), cst)
 	  
     | IsCoFix (i,lar,lfi,vdef) ->
-        let (larv,vdefv,u1) = execute_fix mf env lar lfi vdef in
+        let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in
         let cofix = mkCoFix i larv lfi vdefv in
         check_cofix env cofix;
-	(make_judge cofix larv.(i), u1)
+	(make_judge cofix larv.(i), cst)
 	  
     | IsSort (Prop c) -> 
-	(type_of_prop_or_set c, u0)
+	(type_of_prop_or_set c, cst0)
 
     | IsSort (Type u) ->
-	type_of_type u u0
+	type_of_type u
 	  
     | IsAppL a ->
 	let la = Array.length a in
 	if la = 0 then error_cant_execute CCI env cstr;
 	let hd = a.(0)
 	and tl = Array.to_list (Array.sub a 1 (la - 1)) in
-	let (j,u1) = execute mf env hd in
-	let env1 = set_universes u1 env in
-        let (jl,u2) = execute_list mf env1 tl in
-	let env2 = set_universes u2 env1 in
-	apply_rel_list env2 mf.nocheck jl j
+	let (j,cst1) = execute mf env hd in
+        let (jl,cst2) = execute_list mf env tl in
+	let (j,cst3) = apply_rel_list env mf.nocheck jl j in
+	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
+	(j, cst)
 	    
     | IsLambda (name,c1,c2) -> 
-        let (j,u1) = execute mf env c1 in
+        let (j,cst1) = execute mf env c1 in
         let var = assumption_of_judgment env j in
-	let env1 = push_rel (name,var) (set_universes u1 env) in
-        let (j',u2) = execute mf env1 c2 in 
-	let env2 = set_universes u2 env1 in
-        abs_rel env2 name var j'
+	let env1 = push_rel (name,var) env in
+        let (j',cst2) = execute mf env1 c2 in 
+        let (j,cst3) = abs_rel env1 name var j' in
+	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
+	(j, cst)
 	  
     | IsProd (name,c1,c2) ->
-        let (j,u1) = execute mf env c1 in
+        let (j,cst1) = execute mf env c1 in
         let var = assumption_of_judgment env j in
-	let env1 = push_rel (name,var) (set_universes u1 env) in
-        let (j',u2) = execute mf env1 c2 in
-	let env2 = set_universes u2 env1 in
-        gen_rel env2 name var j'
+	let env1 = push_rel (name,var) env in
+        let (j',cst2) = execute mf env1 c2 in
+	let (j,cst3) = gen_rel env1 name var j' in
+	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
+	(j, cst)
 	  
     | IsCast (c,t) ->
-        let (cj,u1) = execute mf env c in
-	let env1 = set_universes u1 env in
-        let (tj,u2) = execute mf env1 t in
-	let env2 = set_universes u2 env1 in
-        (cast_rel env2 cj tj, u2)
+        let (cj,cst1) = execute mf env c in
+        let (tj,cst2) = execute mf env t in
+	let cst = Constraint.union cst1 cst2 in
+        (cast_rel env cj tj, cst)
 	  
       | _ -> error_cant_execute CCI env cstr
 	  
 and execute_fix mf env lar lfi vdef =
-  let (larj,u1) = execute_array mf env lar in
-  let env1 = set_universes u1 env in
-  let lara = Array.map (assumption_of_judgment env1) larj in
+  let (larj,cst1) = execute_array mf env lar in
+  let lara = Array.map (assumption_of_judgment env) larj in
   let nlara = 
     List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in
-  let env2 = 
-    List.fold_left (fun env nvar -> push_rel nvar env) env1 nlara in
-  let (vdefj,u2) = execute_array mf env2 vdef in
-  let env3 = set_universes u2 env2 in
+  let env1 = 
+    List.fold_left (fun env nvar -> push_rel nvar env) env nlara in
+  let (vdefj,cst2) = execute_array mf env1 vdef in
   let vdefv = Array.map j_val_only vdefj in
-  let u3 = type_fixpoint env3 lfi lara vdefj in
-  (lara,vdefv,u3)
+  let cst3 = type_fixpoint env1 lfi lara vdefj in
+  let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
+  (lara,vdefv,cst)
 
 and execute_array mf env v =
   let (jl,u1) = execute_list mf env (Array.to_list v) in
@@ -160,11 +158,11 @@ and execute_array mf env v =
 
 and execute_list mf env = function
   | [] -> 
-      ([], universes env)
+      ([], Constraint.empty)
   | c::r -> 
-      let (j,u') = execute mf env c in 
-      let (jr,u'') = execute_list mf (set_universes u' env) r in
-      (j::jr, u'')
+      let (j,cst1) = execute mf env c in 
+      let (jr,cst2) = execute_list mf env r in
+      (j::jr, Constraint.union cst1 cst2)
 
 
 (* The typed type of a judgment. *)
@@ -224,19 +222,19 @@ let unsafe_type_of_type env c =
 (* Typing of several terms. *)
 
 let safe_machine_l env cl =
-  let type_one (env,l) c =
-    let (j,u) = safe_machine env c in
-    (set_universes u env, j::l)
+  let type_one (cst,l) c =
+    let (j,cst') = safe_machine env c in
+    (Constraint.union cst cst', j::l)
   in
-  List.fold_left type_one (env,[]) cl
+  List.fold_left type_one (Constraint.empty,[]) cl
 
 let safe_machine_v env cv =
-  let type_one (env,l) c =
-    let (j,u) = safe_machine env c in
-    (set_universes u env, j::l)
+  let type_one (cst,l) c =
+    let (j,cst') = safe_machine env c in
+    (Constraint.union cst cst', j::l)
   in
-  let env',l = Array.fold_left type_one (env,[]) cv in
-  (env', Array.of_list l)
+  let cst',l = Array.fold_left type_one (Constraint.empty,[]) cv in
+  (cst', Array.of_list l)
  
 
 (*s Safe environments. *)
@@ -261,8 +259,8 @@ let lookup_meta = lookup_meta
    being added to the environment. *)
 
 let push_rel_or_var push (id,c) env =
-  let (j,u) = safe_machine env c in
-  let env' = set_universes u env in
+  let (j,cst) = safe_machine env c in
+  let env' = add_constraints cst env in
   let var = assumption_of_judgment env' j in
   push (id,var) env'
 
@@ -279,39 +277,41 @@ let push_rels vars env =
 (* Insertion of constants and parameters in environment. *)
 
 let add_constant sp ce env =
-  let (jb,u) = safe_machine env ce.const_entry_body in
-  let env' = set_universes u env in
-  let (env'',ty) = 
+  let (jb,cst) = safe_machine env ce.const_entry_body in
+  let env' = add_constraints cst env in
+  let (env'',ty,cst') = 
     match ce.const_entry_type with
       | None -> 
-	  env', typed_type_of_judgment env' jb
+	  env', typed_type_of_judgment env' jb, Constraint.empty
       | Some ty -> 
-	  let (jt,u') = safe_machine env ty in
-	  let env'' = set_universes u' env' in
-	  match conv env'' jb.uj_type jt.uj_val with
-	    | Convertible u'' -> 
-		let env'' = set_universes u'' env' in
-		env'', assumption_of_judgment env'' jt
-	    | NotConvertible -> 
-		error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
+	  let (jt,cst') = safe_machine env ty in
+	  let env'' = add_constraints cst' env' in
+	  try
+	    let cst'' = conv env'' jb.uj_type jt.uj_val in
+	    let env'' = add_constraints cst'' env'' in
+	    env'', assumption_of_judgment env'' jt, Constraint.union cst' cst''
+	  with NotConvertible -> 
+	    error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
   in
   let cb = { 
     const_kind = kind_of_path sp;
     const_body = Some (ref (Cooked ce.const_entry_body));
     const_type = ty;
     const_hyps = get_globals (context env);
+    const_constraints = Constraint.union cst cst';
     const_opaque = false } 
   in
   add_constant sp cb env''
 
 let add_parameter sp t env =
-  let (jt,u) = safe_machine env t in
-  let env' = set_universes u env in
+  let (jt,cst) = safe_machine env t in
+  let env' = add_constraints cst env in
   let cb = {
     const_kind = kind_of_path sp;
     const_body = None;
     const_type = assumption_of_judgment env' jt;
     const_hyps = get_globals (context env);
+    const_constraints = cst;
     const_opaque = false } 
   in
   Environ.add_constant sp cb env'
@@ -330,35 +330,32 @@ let rec for_all_prods p env c =
 	 let env' = Environ.push_rel (name,ty) env in
 	 for_all_prods p env' c)
     | DOP2(Prod, b, DLAM(name,c)) -> 
-	let (jb,u) = unsafe_machine env b in
+	let (jb,cst) = unsafe_machine env b in
 	let var = assumption_of_judgment env jb in
 	(p var) &&
-	(let env' = Environ.push_rel (name,var) (set_universes u env) in
+	(let env' = Environ.push_rel (name,var) (add_constraints cst env) in
 	 for_all_prods p env' c)
     | _ -> true
 
 let is_small_type e c = for_all_prods (fun t -> is_small t.typ) e c
 
-let enforce_type_constructor env univ j =
+let enforce_type_constructor env univ j cst =
   match whd_betadeltaiota env j.uj_type with
     | DOP0 (Sort (Type uc)) -> 
-	let u = universes env in
-	set_universes (enforce_geq univ uc u) env
+	Constraint.add (univ,Geq,uc) cst
     | _ -> error "Type of Constructor not well-formed"
 
 let type_one_constructor env_ar nparams ar c =
   let (params,dc) = decompose_prod_n nparams c in
   let env_par = push_rels params env_ar in
-  let (jc,u) = safe_machine env_par dc in
-  let env_par' = set_universes u env_par in
-  let env_par'' = match sort_of_arity env_ar ar with
-    | Type u -> enforce_type_constructor env_par' u jc
-    | Prop _ -> env_par'
+  let (jc,cst) = safe_machine env_par dc in
+  let cst' = match sort_of_arity env_ar ar with
+    | Type u -> enforce_type_constructor env_par u jc cst
+    | Prop _ -> cst
   in
-  let env_ar' = set_universes (universes env_par'') env_ar in
-  let (j,u) = safe_machine env_ar' c in
+  let (j,cst'') = safe_machine env_ar c in
   let issmall = is_small_type env_par c in
-  (set_universes u env_ar', (issmall,j))
+  ((issmall,j), Constraint.union cst' cst'')
 
 let logic_constr env c =
   for_all_prods (fun t -> not (is_info_type env t)) env c
@@ -376,18 +373,19 @@ let is_unit env_par nparams ar spec =
 
 let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,spec) =
   let (lna,vc) = decomp_all_DLAMV_name spec in
-  let (env',(issmall,jlc)) = 
+  let ((issmall,jlc),cst') = 
     List.fold_right
-      (fun c (env,(small,jl)) -> 
-	 let (env',(sm,jc)) = type_one_constructor env nparams ar c in
-	 (env', (small && sm,jc::jl)))
-       (Array.to_list vc) (env_ar,(true,[]))
+      (fun c ((small,jl),cst) -> 
+	 let ((sm,jc),cst') = type_one_constructor env_ar nparams ar c in
+	 ((small && sm,jc::jl), Constraint.union cst cst'))
+      (Array.to_list vc) 
+      ((true,[]),Constraint.empty)
   in
   let castlc = List.map cast_of_judgment jlc in
   let spec' = put_DLAMSV lna (Array.of_list castlc) in
   let isunit = is_unit env_par nparams ar spec in
-  let (_,tyar) = lookup_rel (ninds+1-i) env' in
-  (env', (id,tyar,cnames,issmall,isunit,spec'))
+  let (_,tyar) = lookup_rel (ninds+1-i) env_ar in
+  ((id,tyar,cnames,issmall,isunit,spec'), cst')
 
 let add_mind sp mie env =
   mind_check_names mie;
@@ -401,20 +399,21 @@ let add_mind sp mie env =
   in
   let env_arities = push_rels types_sign env in
   let env_params = push_rels params env_arities in
-  let env_arities',_,inds =
+  let _,inds,cst =
     List.fold_left 
-      (fun (env,i,inds) ind -> 
-	 let (env',ind') = 
-	   type_one_inductive i env env_params nparams ninds ind 
+      (fun (i,inds,cst) ind -> 
+	 let (ind',cst') = 
+	   type_one_inductive i env_arities env_params nparams ninds ind 
 	 in
-	 (env',succ i,ind'::inds))
-      (env_arities,1,[]) mie.mind_entry_inds
+	 (succ i,ind'::inds, Constraint.union cst cst'))
+      (1,[],Constraint.empty) 
+      mie.mind_entry_inds
   in
   let kind = kind_of_path sp in
   let mib = 
-    cci_inductive env env_arities' kind nparams mie.mind_entry_finite inds
+    cci_inductive env env_arities kind nparams mie.mind_entry_finite inds cst
   in
-  add_mind sp mib (set_universes (universes env_arities') env)
+  add_mind sp mib (add_constraints cst env)
 
 let export = export
 let import = import
diff --git a/kernel/typing.mli b/kernel/typing.mli
index 639772946..a960b78dd 100644
--- a/kernel/typing.mli
+++ b/kernel/typing.mli
@@ -57,13 +57,13 @@ val j_val : judgment -> constr
 val j_type : judgment -> constr
 val j_kind : judgment -> constr
 
-val safe_machine : 'a environment -> constr -> judgment * universes
+val safe_machine : 'a environment -> constr -> judgment * constraints
 val safe_machine_type : 'a environment -> constr -> typed_type
 
-val fix_machine : 'a environment -> constr -> judgment * universes
+val fix_machine : 'a environment -> constr -> judgment * constraints
 val fix_machine_type : 'a environment -> constr -> typed_type
 
-val unsafe_machine : 'a environment -> constr -> judgment * universes
+val unsafe_machine : 'a environment -> constr -> judgment * constraints
 val unsafe_machine_type : 'a environment -> constr -> typed_type
 
 val type_of : 'a environment -> constr -> constr
diff --git a/kernel/univ.ml b/kernel/univ.ml
index a5fa727ec..0f6b7185a 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -48,11 +48,6 @@ type arc = Arc of universe * relation
 
 type universes = arc UniverseMap.t
 
-exception UniverseInconsistency
-
-type constraint_function = 
-    universe -> universe -> universes -> universes
-
 (* in Arc(u,Greater(b,v,r))::arcs, we have u>v if b, and u>=v if not b, 
    and r is the next relation pertaining to u; this relation may be
    Greater or Terminal. *)
@@ -244,12 +239,14 @@ let merge_disc g u v =
 
 (* Universe inconsistency: error raised when trying to enforce a relation
    that would create a cycle in the graph of universes. *)
-let error_inconsistency () =
-  raise UniverseInconsistency
+
+exception UniverseInconsistency
+
+let error_inconsistency () = raise UniverseInconsistency
 
 (* enforcegeq : universe -> universe -> unit *)
 (* enforcegeq u v will force u>=v if possible, will fail otherwise *)
-let enforce_geq u v g =
+let enforce_univ_geq u v g =
   let g = declare_univ u g in
   let g = declare_univ v g in
   match compare g u v with
@@ -263,7 +260,7 @@ let enforce_geq u v g =
 
 (* enforceq : universe -> universe -> unit *)
 (* enforceq u v will force u=v if possible, will fail otherwise *)
-let enforce_eq u v g =
+let enforce_univ_eq u v g =
   let g = declare_univ u g in
   let g = declare_univ v g in
   match compare g u v with
@@ -278,7 +275,7 @@ let enforce_eq u v g =
            | EQ -> anomaly "compare")
 
 (* enforcegt u v will force u>v if possible, will fail otherwise *)
-let enforce_gt u v g =
+let enforce_univ_gt u v g =
   let g = declare_univ u g in
   let g = declare_univ v g in
   match compare g u v with
@@ -290,20 +287,50 @@ let enforce_gt u v g =
            | NGE -> setgt g u v
            | _ -> error_inconsistency())
 
-let enforce_relation g u = 
+let enforce_univ_relation g u = 
   let rec enfrec g = function
     | Terminal -> g
-    | Equiv v -> enforce_eq u v g
-    | Greater(false,v,r) -> enfrec (enforce_geq u v g) r
-    | Greater(true,v,r) -> enfrec (enforce_gt u v g) r
+    | Equiv v -> enforce_univ_eq u v g
+    | Greater(false,v,r) -> enfrec (enforce_univ_geq u v g) r
+    | Greater(true,v,r) -> enfrec (enforce_univ_gt u v g) r
   in 
   enfrec g
     
 
 (* Merging 2 universe graphs *)
 let merge_universes sp u1 u2 =
-  UniverseMap.fold (fun _ (Arc(u,r)) g -> enforce_relation g u r) u1 u2
+  UniverseMap.fold (fun _ (Arc(u,r)) g -> enforce_univ_relation g u r) u1 u2
+
+
+
+(* Constraints and sets of consrtaints. *)
+
+type constraint_type = Gt | Geq | Eq
 
+type univ_constraint = universe * constraint_type * universe
+
+module Constraint = Set.Make(
+  struct 
+    type t = univ_constraint 
+    let compare = Pervasives.compare 
+  end)
+		      
+type constraints = Constraint.t
+
+type constraint_function = 
+    universe -> universe -> constraints -> constraints
+
+let enforce_gt u v c = Constraint.add (u,Gt,v) c
+let enforce_geq u v c = Constraint.add (u,Geq,v) c
+let enforce_eq u v c = Constraint.add (u,Eq,v) c
+
+let merge_constraints c g =
+  Constraint.fold 
+    (fun cst g -> match cst with
+       | (u,Gt,v) -> enforce_univ_gt u v g
+       | (u,Geq,v) -> enforce_univ_geq u v g
+       | (u,Eq,v) -> enforce_univ_eq u v g)
+    c g
 
 (* Returns the least upper bound of universes u and v. If they are not
    constrained, then a new universe is created.
@@ -315,25 +342,37 @@ let sup u v g =
     | NGE -> 
 	(match compare g v u with
            | NGE -> 
-	       let w = new_univ u.u_sp in 
-	       let g' = setgeq g w u in
-	       w, setgeq g' w v
-           | _ -> v, g)
-    | _ -> u, g
+	       let w = new_univ u.u_sp in
+	       let c = Constraint.add (w,Geq,u) 
+			 (Constraint.singleton (w,Geq,v)) in
+	       w, c
+           | _ -> v, Constraint.empty)
+    | _ -> u, Constraint.empty
 
 (* Returns a fresh universe, juste above u. Does not create new universes
    for Type_0 (the sort of Prop and Set).
    Used to type the sort u. *)
-let super u g = 
+let super u = 
   if u == prop_univ then 
-    prop_univ_univ, g
+    prop_univ_univ, Constraint.empty
   else if u == prop_univ_univ then 
-    prop_univ_univ_univ, g
+    prop_univ_univ_univ, Constraint.empty
+  else
+    let v = new_univ u.u_sp in
+    let c = Constraint.singleton (v,Gt,u) in
+    v,c
+
+let super_super u =
+  if u == prop_univ then
+    prop_univ_univ, prop_univ_univ_univ, Constraint.empty
+  else if u == prop_univ_univ then 
+    let v = new_univ u.u_sp in
+    prop_univ_univ_univ, v, Constraint.singleton (v,Gt,prop_univ_univ_univ)
   else
-    let g = declare_univ u g in
     let v = new_univ u.u_sp in
-    let g' = enter_arc (Arc(v,Greater(true,u,Terminal))) g in
-    v,g'
+    let w = new_univ u.u_sp in
+    let c = Constraint.add (w,Gt,v) (Constraint.singleton (v,Gt,u)) in
+    v, w, c
 
 (* Pretty-printing *)
 let num_universes g =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 2104fa721..65468be3c 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -23,19 +23,37 @@ type universes
 
 val initial_universes : universes
 
-val super : universe -> universes -> universe * universes
+(*s Constraints. *)
 
-val sup : universe -> universe -> universes -> universe * universes
+type constraint_type = Gt | Geq | Eq
 
-exception UniverseInconsistency
+type univ_constraint = universe * constraint_type * universe
+
+module Constraint : Set.S with type elt = univ_constraint
+
+type constraints = Constraint.t
 
-type constraint_function = 
-    universe -> universe -> universes -> universes
+type constraint_function = universe -> universe -> constraints -> constraints
 
 val enforce_gt : constraint_function
 val enforce_geq : constraint_function
 val enforce_eq : constraint_function
 
-(* pretty-printing. *)
+val super : universe -> universe * constraints
+
+val super_super : universe -> universe * universe * constraints
+
+val sup : universe -> universe -> universes -> universe * constraints
+
+(*s Merge of constraints in a universes graph. 
+  The function [merge_constraints] merges a set of constraints in a given
+  universes graph. It raises the exception [UniverseInconsistency] if the
+  constraints are not satisfiable. *)
+
+exception UniverseInconsistency
+
+val merge_constraints : constraints -> universes -> universes
+
+(*s Pretty-printing of universes. *)
 
 val pr_universes : universes -> Pp.std_ppcmds