amelioration de la structure des univers

elimination des compteurs globaux de metas et d'evars du noyau
nettoyage de safe_typing.ml (plus de flags)


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

12 files changed, 411 insertions, 463 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index d21d5b51c8..ee4666a638 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -181,10 +181,6 @@ let add_mind sp mib env =
 	env_locals = new_locals } in
   { env with env_globals = new_globals }
 
-let meta_ctr=ref 0;;
-
-let new_meta ()=incr meta_ctr;!meta_ctr;;
-
 (* Access functions. *)
   
 let lookup_named_type id env =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 953580b0f8..adbbf0c5ce 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -85,7 +85,6 @@ val add_constant :
   section_path -> constant_body -> env -> env
 val add_mind : 
   section_path -> mutual_inductive_body -> env -> env
-val new_meta : unit -> int
 
 (*s Looks up in environment *)
 
diff --git a/kernel/evd.ml b/kernel/evd.ml
index 9a4d5af6a7..a80f21b521 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -17,10 +17,6 @@ open Sign
 
 type evar = int
 
-let new_evar =
-  let evar_ctr = ref 0 in
-  fun () -> incr evar_ctr; !evar_ctr
-
 type evar_body =
   | Evar_empty 
   | Evar_defined of constr
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 6c0e6a716e..f6192c7e50 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -22,8 +22,6 @@ open Sign
 
 type evar = int
 
-val new_evar : unit -> evar
-
 type evar_body =
   | Evar_empty 
   | Evar_defined of constr
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5eb5199623..fa2384d47d 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -865,6 +865,10 @@ let conv_leq env = fconv CUMUL env
 let convleqkey = Profile.declare_profile "conv_leq";;
 let conv_leq env sigma t1 t2 =
   Profile.profile4 convleqkey conv_leq env sigma t1 t2;;
+
+let convkey = Profile.declare_profile "conv";;
+let conv env sigma t1 t2 =
+  Profile.profile4 convleqkey conv env sigma t1 t2;;
 *)
 
 let conv_forall2 f env sigma v1 v2 =
@@ -1095,9 +1099,23 @@ let rec whd_ise1 sigma c =
   match kind_of_term c with
     | IsEvar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev ->
 	whd_ise1 sigma (existential_value sigma (ev,args))
-    | _ -> c
+    | _ -> collapse_appl c
 
 let nf_ise1 sigma = local_strong (whd_ise1 sigma)
 
 (* A form of [whd_ise1] with type "reduction_function" *)
 let whd_evar env = whd_ise1
+
+(* Expand evars, possibly in the head of an application *)
+let whd_castappevar_stack sigma c = 
+  let rec whrec (c, l as s) =
+    match kind_of_term c with
+      | IsEvar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> 
+	  whrec (existential_value sigma (ev,args), l)
+      | IsCast (c,_) -> whrec (c, l)
+      | IsApp (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
+      | _ -> s
+  in 
+  whrec (c, [])
+
+let whd_castappevar sigma c = applist (whd_castappevar_stack sigma c)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index a47b19242f..ae0640aef0 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -200,6 +200,7 @@ val whd_ise1 : 'a evar_map -> constr -> constr
 val nf_ise1 : 'a evar_map -> constr -> constr
 exception Uninstantiated_evar of int
 val whd_ise : 'a evar_map -> constr -> constr
+val whd_castappevar : 'a evar_map -> constr -> constr
 
 (*s Obsolete Reduction Functions *)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ec3b755232..f72712cc8e 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -30,19 +30,9 @@ let j_type j = body_of_type j.uj_type
 let vect_lift = Array.mapi lift
 let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
 
-(*s The machine flags. 
-   [fix] indicates if we authorize general fixpoints ($\mathit{recarg} < 0$)
-   like [Acc_rec.fw].
-   [nocheck] indicates if we can skip some verifications to accelerate
-   the type inference. *)
-
-type 'a mach_flags = {
-  fix : bool;
-  nocheck : bool }
-
 (* The typing machine without information. *)
 
-let rec execute mf env cstr =
+let rec execute env cstr =
   let cst0 = Constraint.empty in
   match kind_of_term cstr with
     | IsMeta _ ->
@@ -70,23 +60,23 @@ let rec execute mf env cstr =
 	(make_judge cstr (type_of_constructor env Evd.empty c), cst0)
 	  
     | IsMutCase (ci,p,c,lf) ->
-        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 (cj,cst1) = execute env c in
+        let (pj,cst2) = execute env p in
+        let (lfj,cst3) = execute_array env lf in
 	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
         (type_of_case env Evd.empty ci pj cj lfj, cst)
   
     | IsFix ((vn,i as vni),(lar,lfi,vdef)) ->
-        if (not mf.fix) && array_exists (fun n -> n < 0) vn then
+        if array_exists (fun n -> n < 0) vn then
           error "General Fixpoints not allowed";
-        let (larjv,vdefv,cst) = execute_fix mf env lar lfi vdef in
+        let (larjv,vdefv,cst) = execute_fix env lar lfi vdef in
 	let larv = Array.map body_of_type larjv in
         let fix = (vni,(larv,lfi,vdefv)) in
-        if not mf.fix then check_fix env Evd.empty fix;
+        check_fix env Evd.empty fix;
 	(make_judge (mkFix fix) larjv.(i), cst)
 	  
     | IsCoFix (i,(lar,lfi,vdef)) ->
-        let (larjv,vdefv,cst) = execute_fix mf env lar lfi vdef in
+        let (larjv,vdefv,cst) = execute_fix env lar lfi vdef in
 	let larv = Array.map body_of_type larjv in
         let cofix = (i,(larv,lfi,vdefv)) in
         check_cofix env Evd.empty cofix;
@@ -100,121 +90,88 @@ let rec execute mf env cstr =
 	judge_of_type inst_u
 	  
     | IsApp (f,args) ->
-	let (j,cst1) = execute mf env f in
-        let (jl,cst2) = execute_array mf env args in
+	let (j,cst1) = execute env f in
+        let (jl,cst2) = execute_array env args in
 	let (j,cst3) =
-	  apply_rel_list env Evd.empty mf.nocheck (Array.to_list jl) j in
+	  apply_rel_list env Evd.empty false (Array.to_list jl) j in
 	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
 	(j, cst)
 	    
     | IsLambda (name,c1,c2) -> 
-        let (j,cst1) = execute mf env c1 in
+        let (j,cst1) = execute env c1 in
         let var = assumption_of_judgment env Evd.empty j in
 	let env1 = push_rel_assum (name,var) env in
-        let (j',cst2) = execute mf env1 c2 in 
+        let (j',cst2) = execute env1 c2 in 
         let (j,cst3) = abs_rel env1 Evd.empty name var j' in
 	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
 	(j, cst)
 	  
      | IsProd (name,c1,c2) ->
-        let (j,cst1) = execute mf env c1 in
+        let (j,cst1) = execute env c1 in
         let varj = type_judgment env Evd.empty j in
 	let env1 = push_rel_assum (name,varj.utj_val) env in
-        let (j',cst2) = execute mf env1 c2 in
+        let (j',cst2) = execute env1 c2 in
         let varj' = type_judgment env Evd.empty j' in
 	let (j,cst3) = gen_rel env1 Evd.empty name varj varj' in
 	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
 	(j, cst)
 
      | IsLetIn (name,c1,c2,c3) ->
-        let (j1,cst1) = execute mf env c1 in
-        let (j2,cst2) = execute mf env c2 in
+        let (j1,cst1) = execute env c1 in
+        let (j2,cst2) = execute env c2 in
 	let tj2 = assumption_of_judgment env Evd.empty j2 in
 	let ({uj_val = b; uj_type = t},cst0) = cast_rel env Evd.empty j1 tj2 in
-        let (j3,cst3) = execute mf (push_rel_def (name,b,t) env) c3 in
+        let (j3,cst3) = execute (push_rel_def (name,b,t) env) c3 in
 	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
 	({ uj_val = mkLetIn (name, j1.uj_val, tj2, j3.uj_val) ;
 	   uj_type = type_app (subst1 j1.uj_val) j3.uj_type },
 	 Constraint.union cst cst0)
 	  
     | IsCast (c,t) ->
-        let (cj,cst1) = execute mf env c in
-        let (tj,cst2) = execute mf env t in
+        let (cj,cst1) = execute env c in
+        let (tj,cst2) = execute env t in
 	let tj = assumption_of_judgment env Evd.empty tj in
 	let cst = Constraint.union cst1 cst2 in
 	let (j, cst0) = cast_rel env Evd.empty cj tj in
 	(j, Constraint.union cst cst0)
 	  
-and execute_fix mf env lar lfi vdef =
-  let (larj,cst1) = execute_array mf env lar in
+and execute_fix env lar lfi vdef =
+  let (larj,cst1) = execute_array env lar in
   let lara = Array.map (assumption_of_judgment env Evd.empty) larj in
   let nlara = 
     List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in
   let env1 = 
     List.fold_left (fun env nvar -> push_rel_assum nvar env) env nlara in
-  let (vdefj,cst2) = execute_array mf env1 vdef in
+  let (vdefj,cst2) = execute_array env1 vdef in
   let vdefv = Array.map j_val vdefj in
   let cst3 = type_fixpoint env1 Evd.empty 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
+and execute_array env v =
+  let (jl,u1) = execute_list env (Array.to_list v) in
   (Array.of_list jl, u1)
 
-and execute_list mf env = function
+and execute_list env = function
   | [] -> 
       ([], Constraint.empty)
   | c::r -> 
-      let (j,cst1) = execute mf env c in 
-      let (jr,cst2) = execute_list mf env r in
+      let (j,cst1) = execute env c in 
+      let (jr,cst2) = execute_list env r in
       (j::jr, Constraint.union cst1 cst2)
 
 (* The typed type of a judgment. *)
 
-let execute_type mf env constr = 
-  let (j,cst) = execute mf env constr in
+let execute_type env constr = 
+  let (j,cst) = execute env constr in
   (type_judgment env Evd.empty j, cst)
 
 
-(* Exported machines.  First safe machines, with no general fixpoint
-   allowed (the flag [fix] is not set) and all verifications done (the
-   flag [nocheck] is not set). *)
-
-let safe_infer env constr = 
-  let mf = { fix = false; nocheck = false } in
-  execute mf env constr
-
-let safe_infer_type env constr = 
-  let mf = { fix = false; nocheck = false } in
-  execute_type mf env constr
-
-(* Machines with general fixpoint. *)
-
-let fix_machine env constr = 
-  let mf = { fix = true; nocheck = false } in
-  execute mf env constr
-
-let fix_machine_type env constr = 
-  let mf = { fix = true; nocheck = false } in
-  execute_type mf env constr
-
-(* Fast machines without any verification. *)
-
-let unsafe_infer env constr = 
-  let mf = { fix = true; nocheck = true } in
-  execute mf env constr
-
-let unsafe_infer_type env constr = 
-  let mf = { fix = true; nocheck = true } in
-  execute_type mf env constr
-
+(* Exported machines. *)
 
-(* ``Type of'' machines. *)
+let safe_infer env constr = execute env constr
 
-let type_of env c = 
-  let (j,_) = safe_infer env c in
-  nf_betaiota env Evd.empty (body_of_type j.uj_type)
+let safe_infer_type env constr = execute_type env constr
 
 (* Typing of several terms. *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 90703ae964..4f94b904e3 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -78,16 +78,3 @@ val j_type : judgment -> constr
 
 val safe_infer : safe_environment -> constr -> judgment * constraints
 
-(*i For debug
-val fix_machine : safe_environment -> constr -> judgment * constraints
-val fix_machine_type : safe_environment -> constr -> types * constraints
-
-val unsafe_infer : safe_environment -> constr -> judgment * constraints
-val unsafe_infer_type : safe_environment -> constr -> types * constraints
-
-val type_of : safe_environment -> constr -> constr
-
-val type_of_type : safe_environment -> constr -> constr
-val unsafe_type_of : safe_environment -> constr -> constr
-i*)
-
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 17f30408dc..997db29c38 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -45,6 +45,43 @@ let type_judgment env sigma j =
     | IsSort s -> {utj_val = j.uj_val; utj_type = s }
     | _ -> error_not_type CCI env j
 
+
+(************************************************)
+(* Incremental typing rules: builds a typing judgement given the *)
+(* judgements for the subterms. *)
+
+(* Type of sorts *)
+
+(* Prop and Set *)
+
+let judge_of_prop =
+  { uj_val = mkSort prop;
+    uj_type = mkSort type_0 }
+
+let judge_of_set =
+  { uj_val = mkSort spec;
+    uj_type = mkSort type_0 }
+
+let judge_of_prop_contents = function
+  | Null -> judge_of_prop
+  | Pos -> judge_of_set
+
+(* Type of Type(i). *)
+
+let judge_of_type u =
+  let (uu,c) = super u in
+  { uj_val = mkSort (Type u);
+    uj_type = mkSort (Type uu) },
+  c
+
+(*
+let type_of_sort c =
+  match kind_of_term c with
+    | IsSort (Type u) -> let (uu,cst) = super u in Type uu, cst
+    | IsSort (Prop _) -> Type prop_univ, Constraint.empty
+    | _ -> invalid_arg "type_of_sort"
+*)
+
 (* Type of a de Bruijn index. *)
 	  
 let relative env sigma n = 
@@ -100,6 +137,106 @@ let type_of_constant env sigma c
   = Profile.profile3 tockey type_of_constant env sigma c;;
 *)
 
+(* Type of an existential variable. Not used in kernel. *)
+let type_of_existential env sigma ev =
+  Instantiate.existential_type sigma ev
+
+
+(* Type of a lambda-abstraction. *)
+
+let sort_of_product domsort rangsort g =
+  match rangsort with
+    (* Product rule (s,Prop,Prop) *) 
+    | Prop _ -> rangsort, Constraint.empty
+    | Type u2 ->
+        (match domsort with
+           (* Product rule (Prop,Type_i,Type_i) *)
+           | Prop _ -> rangsort, Constraint.empty
+           (* Product rule (Type_i,Type_i,Type_i) *) 
+           | Type u1 -> let (u12,cst) = sup u1 u2 g in Type u12, cst)
+
+(* [abs_rel env sigma name var j] implements the rule
+
+ env, name:typ |- j.uj_val:j.uj_type     env, |- (name:typ)j.uj_type : s
+ -----------------------------------------------------------------------
+          env |- [name:typ]j.uj_val : (name:typ)j.uj_type
+
+  Since all products are defined in the Calculus of Inductive Constructions
+  and no upper constraint exists on the sort $s$, we don't need to compute $s$
+*)
+
+let abs_rel env sigma name var j =
+  { uj_val = mkLambda (name, var, j.uj_val);
+    uj_type = mkProd (name, var, j.uj_type) },
+  Constraint.empty
+
+(* [gen_rel env sigma name (typ1,s1) (typ2,s2)] implements the rule
+
+    env |- typ1:s1       env, name:typ |- typ2 : s2
+    -------------------------------------------------------------------------
+         s' >= (s1,s2), env |- (name:typ)j.uj_val : s'
+
+  where j.uj_type is convertible to a sort s2
+*)
+
+(* Type of an application. *)
+
+let apply_rel_list env sigma nocheck argjl funj =
+  let rec apply_rec n typ cst = function
+    | [] -> 
+	{ uj_val  = applist (j_val funj, List.map j_val argjl);
+          uj_type = type_app (fun _ -> typ) funj.uj_type },
+	cst
+    | hj::restjl ->
+        match kind_of_term (whd_betadeltaiota env sigma typ) with
+          | IsProd (_,c1,c2) ->
+              if nocheck then
+                apply_rec (n+1) (subst1 hj.uj_val c2) cst restjl
+	      else 
+		(try 
+		   let c = conv_leq env sigma (body_of_type hj.uj_type) c1 in
+		   let cst' = Constraint.union cst c in
+		   apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl
+		 with NotConvertible -> 
+		   error_cant_apply_bad_type CCI env sigma
+		     (n,c1,body_of_type hj.uj_type)
+		     funj argjl)
+
+          | _ ->
+	      error_cant_apply_not_functional CCI env funj argjl
+  in 
+  apply_rec 1 (body_of_type funj.uj_type) Constraint.empty argjl
+
+(*
+let applykey = Profile.declare_profile "apply_rel_list";;
+let apply_rel_list env sigma nocheck argjl funj
+  = Profile.profile5 applykey apply_rel_list env sigma nocheck argjl funj;;
+*)
+
+(* Type of product *)
+let gen_rel env sigma name t1 t2 =
+  let (s,g) = sort_of_product t1.utj_type t2.utj_type (universes env) in
+  { uj_val = mkProd (name, t1.utj_val, t2.utj_val);
+    uj_type = mkSort s },
+  g
+
+(* [cast_rel env sigma (typ1,s1) j] implements the rule
+
+    env, sigma |- cj.uj_val:cj.uj_type    cst, env, sigma |- cj.uj_type = t
+    ---------------------------------------------------------------------
+         cst, env, sigma |- cj.uj_val:t
+*)
+
+(* Type of casts *)    
+let cast_rel env sigma cj t =
+  try 
+    let cst = conv_leq env sigma (body_of_type cj.uj_type) t in
+    { uj_val = j_val cj;
+      uj_type = t },
+    cst
+  with NotConvertible ->
+    error_actual_type CCI env cj.uj_val (body_of_type cj.uj_type) t
+
 (* Inductive types. *)
 
 let type_of_inductive env sigma i =
@@ -125,9 +262,6 @@ let type_of_constructor env sigma cstr
   = Profile.profile3 tockey type_of_constructor env sigma cstr;;
 *)
 
-let type_of_existential env sigma ev =
-  Instantiate.existential_type sigma ev
-
 (* Case. *)
 
 let rec mysort_of_arity env sigma c =
@@ -228,9 +362,11 @@ let type_of_case env sigma ci pj cj lfj =
     with Induc ->
       error_case_not_inductive CCI env cj.uj_val (body_of_type cj.uj_type) in
   let (bty,rslty) =
-    type_case_branches env sigma indspec (body_of_type pj.uj_type) pj.uj_val cj.uj_val in
+    type_case_branches env sigma indspec
+      (body_of_type pj.uj_type) pj.uj_val cj.uj_val in
   let kind = mysort_of_arity env sigma (body_of_type pj.uj_type) in
-  check_branches_message env sigma (cj.uj_val,body_of_type cj.uj_type) (bty,lft);
+  check_branches_message env sigma
+    (cj.uj_val,body_of_type cj.uj_type) (bty,lft);
   { uj_val  = mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj);
     uj_type = rslty }
 
@@ -240,127 +376,6 @@ let type_of_case env sigma ci pj cj lfj
   = Profile.profile6 tocasekey type_of_case env sigma ci pj cj lfj;;
 *)
 
-(* Prop and Set *)
-
-let judge_of_prop =
-  { uj_val = mkSort prop;
-    uj_type = mkSort type_0 }
-
-let judge_of_set =
-  { uj_val = mkSort spec;
-    uj_type = mkSort type_0 }
-
-let judge_of_prop_contents = function
-  | Null -> judge_of_prop
-  | Pos -> judge_of_set
-
-(* Type of Type(i). *)
-
-let judge_of_type u =
-  let (uu,uuu,c) = super_super u in
-  { uj_val = mkSort (Type u);
-    uj_type = mkSort (Type uu) },
-  c
-
-let type_of_sort c =
-  match kind_of_term c with
-    | IsSort (Type u) -> let (uu,cst) = super u in Type uu, cst
-    | IsSort (Prop _) -> Type prop_univ, Constraint.empty
-    | _ -> invalid_arg "type_of_sort"
-
-(* Type of a lambda-abstraction. *)
-
-let sort_of_product domsort rangsort g =
-  match rangsort with
-    (* Product rule (s,Prop,Prop) *) 
-    | Prop _ -> rangsort, Constraint.empty
-    | Type u2 ->
-        (match domsort with
-           (* Product rule (Prop,Type_i,Type_i) *)
-           | Prop _ -> rangsort, Constraint.empty
-           (* Product rule (Type_i,Type_i,Type_i) *) 
-           | Type u1 -> let (u12,cst) = sup u1 u2 g in Type u12, cst)
-
-(* [abs_rel env sigma name var j] implements the rule
-
- env, name:typ |- j.uj_val:j.uj_type     env, |- (name:typ)j.uj_type : s
- -----------------------------------------------------------------------
-          env |- [name:typ]j.uj_val : (name:typ)j.uj_type
-
-  Since all products are defined in the Calculus of Inductive Constructions
-  and no upper constraint exists on the sort $s$, we don't need to compute $s$
-*)
-
-let abs_rel env sigma name var j =
-  { uj_val = mkLambda (name, var, j.uj_val);
-    uj_type = mkProd (name, var, j.uj_type) },
-  Constraint.empty
-
-(* [gen_rel env sigma name (typ1,s1) (typ2,s2)] implements the rule
-
-    env |- typ1:s1       env, name:typ |- typ2 : s2
-    -------------------------------------------------------------------------
-         s' >= (s1,s2), env |- (name:typ)j.uj_val : s'
-
-  where j.uj_type is convertible to a sort s2
-*)
-
-let gen_rel env sigma name t1 t2 =
-  let (s,g) = sort_of_product t1.utj_type t2.utj_type (universes env) in
-  { uj_val = mkProd (name, t1.utj_val, t2.utj_val);
-    uj_type = mkSort s },
-  g
-
-(* [cast_rel env sigma (typ1,s1) j] implements the rule
-
-    env, sigma |- cj.uj_val:cj.uj_type    cst, env, sigma |- cj.uj_type = t
-    ---------------------------------------------------------------------
-         cst, env, sigma |- cj.uj_val:t
-*)
-	    
-let cast_rel env sigma cj t =
-  try 
-    let cst = conv_leq env sigma (body_of_type cj.uj_type) t in
-    { uj_val = j_val cj;
-      uj_type = t },
-    cst
-  with NotConvertible ->
-    error_actual_type CCI env cj.uj_val (body_of_type cj.uj_type) t
-
-(* Type of an application. *)
-
-let apply_rel_list env sigma nocheck argjl funj =
-  let rec apply_rec n typ cst = function
-    | [] -> 
-	{ uj_val  = applist (j_val funj, List.map j_val argjl);
-          uj_type = type_app (fun _ -> typ) funj.uj_type },
-	cst
-    | hj::restjl ->
-        match kind_of_term (whd_betadeltaiota env sigma typ) with
-          | IsProd (_,c1,c2) ->
-              if nocheck then
-                apply_rec (n+1) (subst1 hj.uj_val c2) cst restjl
-	      else 
-		(try 
-		   let c = conv_leq env sigma (body_of_type hj.uj_type) c1 in
-		   let cst' = Constraint.union cst c in
-		   apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl
-		 with NotConvertible -> 
-		   error_cant_apply_bad_type CCI env sigma
-		     (n,c1,body_of_type hj.uj_type)
-		     funj argjl)
-
-          | _ ->
-	      error_cant_apply_not_functional CCI env funj argjl
-  in 
-  apply_rec 1 (body_of_type funj.uj_type) Constraint.empty argjl
-
-(*
-let applykey = Profile.declare_profile "apply_rel_list";;
-let apply_rel_list env sigma nocheck argjl funj
-  = Profile.profile5 applykey apply_rel_list env sigma nocheck argjl funj;;
-*)
-
 (* Fixpoints. *)
 
 (* Check if t is a subterm of Rel n, and gives its specification, 
@@ -387,43 +402,50 @@ let rec instantiate_recarg sp lrc ra =
     | Norec          -> Norec
     | Param(k)       -> List.nth lrc k
 
-(* To each inductive definition corresponds an array describing the structure of recursive 
-   arguments for each constructor, we call it the recursive spec of the type 
-   (it has type recargs vect). 
-   For checking the guard, we start from the decreasing argument (Rel n) 
-   with its recursive spec.
-   During checking the guardness condition, we collect patterns variables corresponding 
-   to subterms of n, each of them with its recursive spec.
-   They are organised in a list lst of type (int * recargs) list which is sorted 
-   with respect to the first argument.
-
+(* To each inductive definition corresponds an array describing the
+   structure of recursive arguments for each constructor, we call it
+   the recursive spec of the type (it has type recargs vect).  For
+   checking the guard, we start from the decreasing argument (Rel n)
+   with its recursive spec.  During checking the guardness condition,
+   we collect patterns variables corresponding to subterms of n, each
+   of them with its recursive spec.  They are organised in a list lst
+   of type (int * recargs) list which is sorted with respect to the
+   first argument.
 *)
 
 (*
-f is a function of type  env -> int -> (int * recargs) list -> constr -> 'a 
-c is a branch of an inductive definition corresponding to the spec lrec. 
-mind_recvec is the recursive spec of the inductive definition of the decreasing argument n.
+   f is a function of type
+     env -> int -> (int * recargs) list -> constr -> 'a 
+
+   c is a branch of an inductive definition corresponding to the spec
+   lrec.  mind_recvec is the recursive spec of the inductive
+   definition of the decreasing argument n.
 
-check_term env mind_recvec f n lst (lrec,c) will pass the lambdas of c corresponding 
-to pattern variables and collect possibly new subterms variables and apply f to 
-the body of the branch with the correct env and decreasing arg.
+   check_term env mind_recvec f n lst (lrec,c) will pass the lambdas
+   of c corresponding to pattern variables and collect possibly new
+   subterms variables and apply f to the body of the branch with the
+   correct env and decreasing arg.
 *)
 
 let check_term env mind_recvec f = 
   let rec crec env n lst (lrec,c) = 
     let c' = strip_outer_cast c in 
     match lrec, kind_of_term c' with 
-	(ra::lr,IsLambda (x,a,b))
-	-> let lst' = map_lift_fst lst and env' = push_rel_assum (x,a) env and n'=n+1 
-        in begin match ra with 
-	    Mrec(i) -> crec env' n' ((1,mind_recvec.(i))::lst') (lr,b)
-          | Imbr((sp,i) as ind_sp,lrc) ->           
-	       let sprecargs = mis_recargs (lookup_mind_specif (ind_sp,[||]) env) in
-               let lc = Array.map (List.map (instantiate_recarg sp lrc)) sprecargs.(i)
-               in crec env' n' ((1,lc)::lst') (lr,b)
-	  | _ -> crec env' n' lst' (lr,b) end
-	| (_,_) -> f env n lst c'
- in crec env
+	(ra::lr,IsLambda (x,a,b)) ->
+          let lst' = map_lift_fst lst
+          and env' = push_rel_assum (x,a) env
+          and n'=n+1 
+          in begin match ra with 
+	      Mrec(i) -> crec env' n' ((1,mind_recvec.(i))::lst') (lr,b)
+            | Imbr((sp,i) as ind_sp,lrc) ->           
+	        let sprecargs =
+                  mis_recargs (lookup_mind_specif (ind_sp,[||]) env) in
+                let lc = Array.map
+                  (List.map (instantiate_recarg sp lrc)) sprecargs.(i)
+                in crec env' n' ((1,lc)::lst') (lr,b)
+	    | _ -> crec env' n' lst' (lr,b) end
+      | (_,_) -> f env n lst c'
+  in crec env
 
 (* c is supposed to be in beta-delta-iota head normal form *)
 
@@ -433,13 +455,15 @@ let is_inst_var k c =
     | _ -> false
 
 (* 
-is_subterm_specif env sigma lcx mind_recvec n lst c 
-n is the principal arg and has recursive spec lcx, lst is the list of subterms of n with 
-spec. 
-is_subterm_specif should test if c is a subterm of n and fails with Not_found if not.
-In case it is, it should send its recursive specification.
-This recursive spec should be the same size as the number of constructors of the type 
-of c. A problem occurs when c is built by contradiction. In that case no spec is given.
+   is_subterm_specif env sigma lcx mind_recvec n lst c 
+
+   n is the principal arg and has recursive spec lcx, lst is the list
+   of subterms of n with spec.  is_subterm_specif should test if c is
+   a subterm of n and fails with Not_found if not.  In case it is, it
+   should send its recursive specification.  This recursive spec
+   should be the same size as the number of constructors of the type
+   of c. A problem occurs when c is built by contradiction. In that
+   case no spec is given.
 
 *)
 let is_subterm_specif env sigma lcx mind_recvec = 
@@ -474,10 +498,10 @@ let is_subterm_specif env sigma lcx mind_recvec =
           let theBody = bodies.(i)   in
           let sign,strippedBody = decompose_lam_n_assum (decrArg+1) theBody in
           let nbOfAbst = nbfix+decrArg+1 in
-(* when proving that the fixpoint f(x)=e is less than n, it is enough to prove 
-   that e is less than n assuming f is less than n
-   furthermore when f is applied to a term which is strictly less than n, one may 
-   assume that x itself is strictly less than n
+(* when proving that the fixpoint f(x)=e is less than n, it is enough
+   to prove that e is less than n assuming f is less than n
+   furthermore when f is applied to a term which is strictly less than
+   n, one may assume that x itself is strictly less than n
 *)
           let newlst = 
             let lst' = (nbOfAbst,lcx) :: (map_lift_fst_n nbOfAbst lst) in
@@ -609,16 +633,18 @@ let rec check_subterm_rec_meta env sigma vectn k def =
 	       array_for_all (check_rec_call env' n' lst') bodies
             else 
               let theDecrArg  = List.nth l decrArg in
-		begin
-		  try 
-		    match is_subterm_specif env sigma lcx mind_recvec n lst theDecrArg
-		    with Some recArgsDecrArg -> 
-		       let theBody = bodies.(i)   in
-			 check_rec_call_fix_body env' n' lst' (decrArg+1) recArgsDecrArg
-			    theBody
-		      | None -> array_for_all (check_rec_call env' n' lst') bodies
-		  with Not_found -> array_for_all (check_rec_call env' n' lst') bodies
-		end
+	      (try 
+		match
+                  is_subterm_specif env sigma lcx mind_recvec n lst theDecrArg
+		with
+                    Some recArgsDecrArg -> 
+		      let theBody = bodies.(i)   in
+		      check_rec_call_fix_body
+                        env' n' lst' (decrArg+1) recArgsDecrArg theBody
+		  | None ->
+                      array_for_all (check_rec_call env' n' lst') bodies
+	      with Not_found ->
+                array_for_all (check_rec_call env' n' lst') bodies)
 
 	| IsCast (a,b) -> 
 	    (check_rec_call env n lst a) &&
@@ -879,7 +905,8 @@ let type_fixpoint env sigma lna lar vdefj =
 	 try conv_leq env sigma def (lift lt ar) 
 	 with NotConvertible -> raise (IllBranch i))
       env sigma
-      (Array.map (fun j -> body_of_type j.uj_type) vdefj) (Array.map body_of_type lar)
+      (Array.map (fun j -> body_of_type j.uj_type) vdefj)
+      (Array.map body_of_type lar)
   with IllBranch i ->
     error_ill_typed_rec_body CCI env i lna vdefj lar
 
@@ -911,5 +938,3 @@ let control_only_guard env sigma =
     | IsLetIn (_,c1,c2,c3) -> control_rec c1; control_rec c2; control_rec c3
   in 
   control_rec 
-
-    
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index b2db983734..aaa07142f3 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -33,33 +33,28 @@ val assumption_of_judgment :
 val type_judgment : 
   env -> 'a evar_map -> unsafe_judgment -> unsafe_type_judgment
 
-val relative : env -> 'a evar_map -> int -> unsafe_judgment
+(*s Type of sorts. *)
+val judge_of_prop_contents : contents -> unsafe_judgment
 
-val type_of_constant : env -> 'a evar_map -> constant -> types
+val judge_of_type : universe -> unsafe_judgment * constraints
 
-val type_of_inductive : env -> 'a evar_map -> inductive -> types
+(*s Type of atomic terms. *)
+val relative : env -> 'a evar_map -> int -> unsafe_judgment
 
-val type_of_constructor : env -> 'a evar_map -> constructor -> types
+val type_of_constant : env -> 'a evar_map -> constant -> types
 
 val type_of_existential : env -> 'a evar_map -> existential -> types
 
-val type_of_case : env -> 'a evar_map -> case_info
-  -> unsafe_judgment -> unsafe_judgment 
-    -> unsafe_judgment array -> unsafe_judgment
-
-val type_case_branches :
-  env -> 'a evar_map -> Inductive.inductive_type -> constr -> types
-    -> constr -> types array * types
-
-val judge_of_prop_contents : contents -> unsafe_judgment
-
-val judge_of_type : universe -> unsafe_judgment * constraints
-
 (*s Type of an abstraction. *)
 val abs_rel : 
   env -> 'a evar_map -> name -> types -> unsafe_judgment 
     -> unsafe_judgment * constraints
 
+(*s Type of application. *)
+val apply_rel_list : 
+  env -> 'a evar_map -> bool -> unsafe_judgment list -> unsafe_judgment
+    -> unsafe_judgment * constraints
+
 (*s Type of a product. *)
 val gen_rel :
   env -> 'a evar_map -> name -> unsafe_type_judgment -> unsafe_type_judgment 
@@ -72,22 +67,33 @@ val cast_rel :
   env -> 'a evar_map -> unsafe_judgment -> types
     -> unsafe_judgment * constraints
 
-val apply_rel_list : 
-  env -> 'a evar_map -> bool -> unsafe_judgment list -> unsafe_judgment
-    -> unsafe_judgment * constraints
+(*s Inductive types. *)
+open Inductive
 
-val check_fix : env -> 'a evar_map -> fixpoint -> unit
-val check_cofix : env -> 'a evar_map -> cofixpoint -> unit
-val control_only_guard : env -> 'a evar_map -> constr -> unit
+val type_of_inductive : env -> 'a evar_map -> inductive -> types
 
-val type_fixpoint : env -> 'a evar_map -> name list -> types array 
-    -> unsafe_judgment array -> constraints
+val type_of_constructor : env -> 'a evar_map -> constructor -> types
 
-open Inductive
+(*s Type of Cases. *)
+val type_of_case : env -> 'a evar_map -> case_info
+  -> unsafe_judgment -> unsafe_judgment 
+    -> unsafe_judgment array -> unsafe_judgment
 
 val find_case_dep_nparams :
   env -> 'a evar_map -> constr * constr -> inductive_family -> constr -> bool
 
+val type_case_branches :
+  env -> 'a evar_map -> Inductive.inductive_type -> constr -> types
+    -> constr -> types array * types
+
+(*s Type of fixpoints and guard condition. *)
+val check_fix : env -> 'a evar_map -> fixpoint -> unit
+val check_cofix : env -> 'a evar_map -> cofixpoint -> unit
+val type_fixpoint : env -> 'a evar_map -> name list -> types array 
+    -> unsafe_judgment array -> constraints
+
+val control_only_guard : env -> 'a evar_map -> constr -> unit
+
 (*i
 val hyps_inclusion : env -> 'a evar_map -> named_context -> named_context -> bool
 i*)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index fc5e4ff23e..e8f6923003 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -48,110 +48,118 @@ let new_univ =
   let univ_gen = ref 0 in
   (fun sp -> incr univ_gen; { u_mod = !current_module; u_num = !univ_gen })
 
-type relation = 
-  | Greater of bool * universe * relation (* if bool then > else >= *)
-  | Equiv of universe
-  | Terminal
+(* Comparison on this type is pointer equality *)
+type canonical_arc =
+    { univ: universe; gt: universe list; ge: universe list }
 
-module UniverseMap = Map.Make(UniverseOrdered)
+let terminal u = {univ=u; gt=[]; ge=[]}
 
-type arc = Arc of universe * relation
+(* A universe is either an alias for another one, or a canonical one,
+   for which we know the universes that are smaller *)
+type univ_entry =
+    Canonical of canonical_arc
+  | Equiv of universe * universe
 
-type universes = arc UniverseMap.t
+module UniverseMap = Map.Make(UniverseOrdered)
 
-(* 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. *)
+type universes = univ_entry UniverseMap.t
 		   
-let enter_arc a g =
-  let Arc(i,_) = a in
-  UniverseMap.add i a g
+let enter_equiv_arc u v g =
+  UniverseMap.add u (Equiv(u,v)) g
+
+let enter_arc ca g =
+  UniverseMap.add ca.univ (Canonical ca) g
 
 let declare_univ u g =
   if not (UniverseMap.mem u g) then
-    UniverseMap.add u (Arc(u,Terminal)) g
+    enter_arc (terminal u) g
   else
     g
 
-(* The universes of Prop and Set: Type_0, Type_1 and Type_2, and the
+(* The universes of Prop and Set: Type_0, Type_1 and the
    resulting graph. *)
-let (initial_universes,prop_univ,prop_univ_univ,prop_univ_univ_univ) =
+let (initial_universes,prop_univ,prop_univ_univ) =
   let prop_sp = ["prop_univ"] in
   let u = { u_mod = prop_sp; u_num = 0 } in
   let su = { u_mod = prop_sp; u_num = 1 } in
-  let ssu = { u_mod = prop_sp; u_num = 2 } in
-  let g = enter_arc (Arc(u,Terminal)) UniverseMap.empty in
-  let g = enter_arc (Arc(su,Terminal)) g in
-  let g = enter_arc (Arc(ssu,Terminal)) g in
-  let g = enter_arc (Arc(su,Greater(true,u,Terminal))) g in
-  let g = enter_arc (Arc(ssu,Greater(true,su,Terminal))) g in
-  (g,u,su,ssu)
+  let g = enter_arc (terminal u) UniverseMap.empty in
+  let g = enter_arc {univ=su; gt=[u]; ge=[]} g in
+  (g,u,su)
 
 (* Every universe has a unique canonical arc representative *)
 
-(* repr : universes -> universe -> arc *)
+(* repr : universes -> universe -> canonical_arc *)
 (* canonical representative : we follow the Equiv links *)
 let repr g u = 
   let rec repr_rec u =
-    let arc =
+    let a =
       try UniverseMap.find u g
       with Not_found -> anomalylabstrm "Impuniv.repr"
 	  [< 'sTR"Universe "; pr_uni u; 'sTR" undefined" >] 
     in
-    match arc with 
-      | Arc(_,Equiv(v)) -> repr_rec v
-      | _ -> arc
+    match a with 
+      | Equiv(_,v) -> repr_rec v
+      | Canonical arc -> arc
   in
   repr_rec u
 
 let can g = List.map (repr g)
 
 (* transitive closure : we follow the Greater links *)
-(* close : relation -> universe list * universe list *)
-let close = 
-  let rec closerec ((u,v) as pair) = function
-    | Terminal -> pair
-    | Greater(true,v_0,r)  -> closerec (v_0::u,v) r
-    | Greater(false,v_0,r) -> closerec (u,v_0::v) r
-    | _ -> anomaly "Wrong universe structure"
+
+(* collect : canonical_arc -> canonical_arc list * canonical_arc list *)
+(* collect u = (V,W) iff V={v canonical | u>v} W={w canonical | u>=w}-V *)
+(* i.e. collect does the transitive closure of what is known about u *)
+let collect g arcu = 
+  let rec coll_rec gt ge = function
+    | [],[] -> (gt, list_subtractq ge gt)
+    | arcv::gt', ge' ->
+	if List.memq arcv gt then 
+	  coll_rec gt ge (gt',ge')
+	else
+          coll_rec (arcv::gt) ge ((can g (arcv.gt@arcv.ge))@gt',ge')
+    | [], arcw::ge' -> 
+	if (List.memq arcw gt) or (List.memq arcw ge) then 
+	  coll_rec gt ge ([],ge')
+	else
+          coll_rec gt (arcw::ge) (can g arcw.gt, (can g arcw.ge)@ge')
   in 
-  closerec ([],[]) 
+  coll_rec [] [] ([],[arcu])
 
-(* reprgeq : arc -> arc list *)
+(* reprgeq : canonical_arc -> canonical_arc list *)
 (* All canonical arcv such that arcu>=arcc with arcv#arcu *)
-let reprgeq g (Arc(_,ru) as arcu) =
-  let (_,v) = close ru in
+let reprgeq g arcu =
   let rec searchrec w = function
     | [] -> w
-    | v_0 :: v ->
-	let arcv = repr g v_0 in
-        if List.memq arcv w || arcu=arcv then 
-	  searchrec w v
+    | v :: vl ->
+	let arcv = repr g v in
+        if List.memq arcv w || arcu==arcv then 
+	  searchrec w vl
         else 
-	  searchrec (arcv :: w) v
+	  searchrec (arcv :: w) vl
   in 
-  searchrec [] v
+  searchrec [] arcu.ge
+
+(* between : universe -> canonical_arc -> canonical_arc list *)
+(* between u v = {w|u>=w>=v, w canonical}          *)     
+(* between is the most costly operation *)
+let between g u arcv = 
+  let rec explore (memo,l) arcu = 
+    try 
+      memo,list_unionq (List.assq arcu memo) l (* when memq arcu memo *)
+    with Not_found ->
+      let w = reprgeq g arcu in
+      let (memo',sols) = List.fold_left explore (memo,[]) w in
+      let sols' = if sols=[] then [] else arcu::sols in
+      ((arcu,sols')::memo', list_unionq sols' l) 
+  in
+  snd (explore ([(arcv,[arcv])],[]) (repr g u))
+
+(* We assume  compare(u,v) = GE with v canonical (see compare below).
+   In this case List.hd(between g u v) = repr u
+   Otherwise, between g u v = [] 
+ *)
 
-(* collect : arc -> arc list * arc list *)
-(* collect u = (V,W) iff V={v canonical | u>v} W={w canonical | u>=w}-V *)
-(* i.e. collect does the transitive closure of what is known about u *)
-let collect g u = 
-  let rec coll_rec v w = function
-    | [],[] -> (v,list_subtractq w v)
-    | (Arc(_,rv) as arcv)::v',w' ->
-	if List.memq arcv v then 
-	  coll_rec v w (v',w')
-	else
-          let (gt,geq) = close rv in
-          coll_rec (arcv::v) w ((can g (gt@geq))@v',w')
-    | [],(Arc(_,rw) as arcw)::w' -> 
-	if (List.memq arcw v) or (List.memq arcw w) then 
-	  coll_rec v w ([],w')
-	else
-          let (gt,geq) = close rw in
-          coll_rec v (arcw::w) (can g gt, (can g geq)@w')
-  in 
-  coll_rec [] [] ([],[u])
 
 type order = EQ | GT | GE | NGE
 
@@ -159,13 +167,13 @@ type order = EQ | GT | GE | NGE
 let compare g u v = 
   let arcu = repr g u 
   and arcv = repr g v in
-  if arcu=arcv then 
+  if arcu==arcv then 
     EQ
   else 
-    let (v,w) = collect g arcu in
-    if List.memq arcv v then 
+    let (gt,geq) = collect g arcu in
+    if List.memq arcv gt then 
       GT
-    else if List.memq arcv w then 
+    else if List.memq arcv geq then 
       GE
     else 
       NGE
@@ -179,29 +187,12 @@ let compare g u v =
    Adding u>v is consistent iff compare(v,u) = NGE 
     and then it is redundant iff compare(u,v) = GT *)
 
-(* between : universe -> arc -> arc list *)
-(* we assume  compare(u,v) = GE with v canonical    *)
-(* between u v = {w|u>=w>=v, w canonical}          *)     
-let between g u arcv = 
-  let rec explore (memo,l) arcu = 
-    try 
-      memo,list_unionq (List.assq arcu memo) l (* when memq arcu memo *)
-    with Not_found ->
-      let w = reprgeq g arcu in
-      let (memo',sols) = List.fold_left explore (memo,[]) w in
-      let sols' = if sols=[] then [] else arcu::sols in
-      ((arcu,sols')::memo', list_unionq sols' l) 
-  in
-  snd (explore ([(arcv,[arcv])],[]) (repr g u))
-
-(* Note: hd(between u v) = repr u  *)
-(* between is the most costly operation *)
 
 (* setgt : universe -> universe -> unit *)
 (* forces u > v *)
 let setgt g u v =
-  let Arc(u',ru) = repr g u in
-  enter_arc (Arc(u',Greater(true,v,ru))) g
+  let arcu = repr g u in
+  enter_arc {arcu with gt=v::arcu.gt} g
 
 (* checks that non-redondant *)
 let setgt_if g u v = match compare g u v with
@@ -211,8 +202,8 @@ let setgt_if g u v = match compare g u v with
 (* setgeq : universe -> universe -> unit *)
 (* forces u >= v *)
 let setgeq g u v =
-  let Arc(u',ru) = repr g u in
-  enter_arc (Arc(u',Greater(false,v,ru))) g
+  let arcu = repr g u in
+  enter_arc {arcu with ge=v::arcu.ge} g
 
 
 (* checks that non-redondant *)
@@ -225,15 +216,15 @@ let setgeq_if g u v = match compare g u v with
 (* merge u v  forces u ~ v with repr u as canonical repr *)
 let merge g u v =
   match between g u (repr g v) with
-    | Arc(u',_)::v ->
-	let redirect (g,w,w') (Arc(v',rv)) =
-       	  let v,v'_0 = close rv in
- 	  let g' = enter_arc (Arc(v',Equiv(u'))) g in
- 	  (g',list_unionq v w,v'_0@w') 
+    | arcu::v -> (* arcu is chosen as canonical and all others (v) are *)
+                 (* redirected to it *)
+	let redirect (g,w,w') arcv =
+ 	  let g' = enter_equiv_arc arcv.univ arcu.univ g in
+ 	  (g',list_unionq arcv.gt w,arcv.ge@w') 
 	in
 	let (g',w,w') = List.fold_left redirect (g,[],[]) v in
-	let g'' = List.fold_left (fun g -> setgt_if g u') g' w in
-	let g''' = List.fold_left (fun g -> setgeq_if g u') g'' w' in
+	let g'' = List.fold_left (fun g -> setgt_if g arcu.univ) g' w in
+	let g''' = List.fold_left (fun g -> setgeq_if g arcu.univ) g'' w' in
 	g'''
     | [] -> anomaly "between"
 
@@ -241,11 +232,11 @@ let merge g u v =
 (* we assume  compare(u,v) = compare(v,u) = NGE *)
 (* merge_disc u v  forces u ~ v with repr u as canonical repr *)
 let merge_disc g u v =
-  let (Arc(u',_), Arc(v',rv)) = (repr g u, repr g v) in
-  let v,v'_0 = close rv in
-  let g' = enter_arc (Arc(v',Equiv(u'))) g in
-  let g'' = List.fold_left (fun g -> setgt_if g u') g' v in
-  let g''' = List.fold_left (fun g -> setgeq_if g u') g'' v'_0 in
+  let arcu = repr g u in
+  let arcv = repr g v in
+  let g' = enter_equiv_arc arcv.univ arcu.univ g in
+  let g'' = List.fold_left (fun g -> setgt_if g arcu.univ) g' arcv.gt in
+  let g''' = List.fold_left (fun g -> setgeq_if g arcu.univ) g'' arcv.ge in
   g'''
 
 (* Universe inconsistency: error raised when trying to enforce a relation
@@ -298,19 +289,16 @@ let enforce_univ_gt u v g =
            | NGE -> setgt g u v
            | _ -> error_inconsistency())
 
-let enforce_univ_relation g u = 
-  let rec enfrec g = function
-    | Terminal -> g
-    | 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
-    
+let enforce_univ_relation g = function 
+  | Equiv (u,v) -> enforce_univ_eq u v g
+  | Canonical {univ=u; gt=gt; ge=ge} ->
+      let g' = List.fold_right (enforce_univ_gt u) gt g in
+      List.fold_right (enforce_univ_geq u) ge g'
+
 
 (* Merging 2 universe graphs *)
 let merge_universes sp u1 u2 =
-  UniverseMap.fold (fun _ (Arc(u,r)) g -> enforce_univ_relation g u r) u1 u2
+  UniverseMap.fold (fun _ a g -> enforce_univ_relation g a) u1 u2
 
 
 
@@ -343,6 +331,17 @@ let merge_constraints c g =
        | (u,Eq,v) -> enforce_univ_eq u v g)
     c g
 
+(* 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 = 
+  if u == prop_univ then 
+    prop_univ_univ, Constraint.empty
+  else
+    let v = new_univ () in
+    let c = Constraint.singleton (v,Gt,u) in
+    v,c
+
 (* Returns the least upper bound of universes u and v. If they are not
    constrained, then a new universe is created.
    Used to type the products. *)
@@ -360,61 +359,30 @@ let sup u v g =
            | _ -> 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 = 
-  if u == prop_univ then 
-    prop_univ_univ, Constraint.empty
-  else if u == prop_univ_univ then 
-    prop_univ_univ_univ, Constraint.empty
-  else
-    let v = new_univ () 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 () in
-    prop_univ_univ_univ, v, Constraint.singleton (v,Gt,prop_univ_univ_univ)
-  else
-    let v = new_univ () in
-    let w = new_univ () in
-    let c = Constraint.add (w,Gt,v) (Constraint.singleton (v,Gt,u)) in
-    v, w, c
-
 (* Pretty-printing *)
 let num_universes g =
   UniverseMap.fold (fun _ _ -> succ) g 0
 
 let num_edges g =
-  let reln_len = 
-    let rec lenrec n = function
-      | Terminal -> n
-      | Equiv _ -> n+1
-      | Greater(_,_,r) -> lenrec (n+1) r
-    in 
-    lenrec 0 
+  let reln_len = function
+    | Equiv _ -> 1
+    | Canonical {gt=gt;ge=ge} -> List.length gt + List.length ge
   in
-  UniverseMap.fold (fun _ (Arc(_,r)) n -> n + (reln_len r)) g 0
+  UniverseMap.fold (fun _ a n -> n + (reln_len a)) g 0
     
-let pr_reln u r = 
-  let rec prec = function
-    | Greater(true,v,r) -> 
-	[< pr_uni u ; 'sTR">" ; pr_uni v ; 'fNL ; prec r >]
-    | Greater(false,v,r) -> 
-	[< pr_uni u ; 'sTR">=" ; pr_uni v ; 'fNL ; prec r >]
-    | Equiv v -> 
-	[< pr_uni u ; 'sTR"=" ; pr_uni v >]
-    | Terminal -> [< >]
-  in 
-  prec r
+let pr_arc = function 
+  | Canonical {univ=u; gt=gt; ge=ge} -> 
+      hOV 2
+        [< pr_uni u; 'sPC;
+           prlist_with_sep pr_spc (fun v -> [< 'sTR">"; pr_uni v >]) gt;
+           prlist_with_sep pr_spc (fun v -> [< 'sTR">="; pr_uni v >]) ge
+        >]
+  | Equiv (u,v) -> 
+      [< pr_uni u ; 'sTR"=" ; pr_uni v >]
 
 let pr_universes g =
   let graph = UniverseMap.fold (fun k a l -> (k,a)::l) g [] in
-  prlist_with_sep pr_fnl (function (_,Arc(u,r)) -> pr_reln u r) graph
+  prlist_with_sep pr_fnl (function (_,a) -> pr_arc a) graph
     
 
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 3aedf921e0..4348a65415 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -21,7 +21,6 @@ val implicit_univ : universe
 
 val prop_univ : universe
 val prop_univ_univ : universe
-val prop_univ_univ_univ : universe
 
 val set_module : dir_path -> unit
 
@@ -51,8 +50,6 @@ val enforce_eq : constraint_function
 
 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.