Suites modifs du noyau. Univ devient purement fonctionnel.

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

20 files changed, 227 insertions, 322 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 4bb9c941f..3b2655af6 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -415,7 +415,7 @@ let defined_vars flags env =
 	 match b with
 	   | None -> e
 	   | Some body -> (id, body)::e)
-      env []
+      env ~init:[]
 (*  else []*)
 
 let defined_rels flags env =
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 4fb1663d0..3b901a1ac 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -143,6 +143,6 @@ let cook_constant env r =
           (map_named_declaration (expmod_constr r.d_modlist) d)
           ctxt)
       cb.const_hyps
-      empty_named_context in
+      ~init:empty_named_context in
   let body,typ = abstract_constant r.d_abstract hyps (body,typ) in
   (body, typ, cb.const_constraints, cb.const_opaque)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 757fa34b0..ff280fa15 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -79,10 +79,10 @@ let reset_rel_context env =
 
 
 
-let fold_named_context f env a =
+let fold_named_context f env ~init =
   snd (Sign.fold_named_context
 	 (fun d (env,e) -> (push_named_decl d env, f env d e))
-         (named_context env) (reset_context env,a))
+         (named_context env) (reset_context env,init))
 
 let fold_named_context_reverse f a env =
   Sign.fold_named_context_reverse f a (named_context env) 
@@ -97,10 +97,10 @@ let push_rec_types (lna,typarray,_) env =
   Array.fold_left
     (fun e assum -> push_rel_assum assum e) env ctxt
 
-let fold_rel_context f env a =
-  snd (List.fold_right
+let fold_rel_context f env ~init =
+  snd (fold_rel_context
 	 (fun d (env,e) -> (push_rel d env, f env d e))
-         (rel_context env) (reset_rel_context env,a))
+         (rel_context env) (reset_rel_context env,init))
 
 let set_universes g env =
   if env.env_universes == g then env else { env with env_universes = g }
@@ -184,19 +184,26 @@ let global_vars_set env constr =
    contained in the types of the needed variables. *)
 
 let keep_hyps env needed =
-  let rec keep_rec needed = function
-  | (id,copt,t as d) ::sign when Idset.mem id needed ->
-      let globc = 
-	match copt with
-	  | None -> Idset.empty
-	  | Some c -> global_vars_set env c in
-      let needed' =
-	Idset.union (global_vars_set env (body_of_type t)) 
-	  (Idset.union globc needed) in
-      d :: (keep_rec needed' sign)
-  | _::sign -> keep_rec needed sign
-  | [] -> [] in
-  keep_rec needed (named_context env)
+  let really_needed =
+    Sign.fold_named_context_reverse
+      (fun need (id,copt,t) ->
+        if Idset.mem id need then
+          let globc = 
+	    match copt with
+	      | None -> Idset.empty
+	      | Some c -> global_vars_set env c in
+	  Idset.union
+            (global_vars_set env (body_of_type t)) 
+	    (Idset.union globc need)
+        else need)
+      ~init:needed
+      (named_context env) in
+  Sign.fold_named_context
+    (fun (id,_,_ as d) nsign ->
+      if Idset.mem id really_needed then add_named_decl d nsign
+      else nsign)
+    (named_context env)
+    ~init:empty_named_context
 
 
 (* Constants *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 83915157a..8e1d848de 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -47,14 +47,15 @@ val push_rec_types : rec_declaration -> env -> env
 
 (*s Recurrence on [named_context]: older declarations processed first *)
 val fold_named_context :
-  (env -> named_declaration -> 'a -> 'a) -> env -> 'a -> 'a
+  (env -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
 
 (* Recurrence on [named_context] starting from younger decl *)
 val fold_named_context_reverse :
-  ('a -> named_declaration -> 'a) -> 'a -> env -> 'a
+  ('a -> named_declaration -> 'a) -> init:'a -> env -> 'a
 
 (*s Recurrence on [rel_context] *)
-val fold_rel_context : (env -> rel_declaration -> 'a -> 'a) -> env -> 'a -> 'a
+val fold_rel_context :
+  (env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
 
 (*s add entries to environment *)
 val set_universes : universes -> env -> env
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 32303a6fa..a5224914b 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -461,18 +461,6 @@ let is_recursive listind =
   in 
   array_exists one_is_rec
 
-let abstract_inductive ntypes hyps (par,np,id,arity,cnames,issmall,isunit,lc) =
-  let args = instance_from_named_context (List.rev hyps) in
-  let nhyps = List.length hyps in
-  let nparams = Array.length args in (* nparams = nhyps - nb(letin) *)
-  let new_refs =
-    list_tabulate (fun k -> mkApp (mkRel (k+nhyps+1),args)) ntypes in
-  let abs_constructor b = it_mkNamedProd_or_LetIn (substl new_refs b) hyps in
-  let lc' = Array.map abs_constructor lc in
-  let arity' = it_mkNamedProd_or_LetIn arity hyps in
-  let par' = push_named_to_rel_context hyps par in
-  (par',np+nparams,id,arity',cnames,issmall,isunit,lc')
-
 let cci_inductive env env_ar finite inds cst =
   let ntypes = List.length inds in
   let ids = 
@@ -507,7 +495,7 @@ let cci_inductive env env_ar finite inds cst =
       mind_nf_lc = nf_lc;
       mind_user_arity  = ar;
       mind_nf_arity = nf_ar;
-      mind_nrealargs = List.length ar_sign - nparams;
+      mind_nrealargs = rel_context_length ar_sign - nparams;
       mind_sort = ar_sort;
       mind_kelim = kelim;
       mind_listrec = recargs;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 06219f084..4cfc1d2af 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -81,19 +81,22 @@ let constructor_instantiate mispec =
   substl s
 
 (* Instantiate the parameters of the inductive type *)
+(* TODO: verify the arg of LetIn correspond to the value in the
+   signature ? *)
 let instantiate_params t args sign =
-  let rec inst s t = function
-    | ((_,None,_)::ctxt,a::args) ->
-	(match kind_of_term t with
-	   | Prod(_,_,t) -> inst (a::s) t (ctxt,args)
-	   | _ -> anomaly"instantiate_params: type, ctxt and args mismatch")
-    | ((_,(Some b),_)::ctxt,args) -> 
-	(match kind_of_term t with
-	   | LetIn(_,_,_,t) -> inst ((substl s b)::s) t (ctxt,args)
-	   | _ -> anomaly"instantiate_params: type, ctxt and args mismatch")
-    | [], [] -> substl s t
-    | _ -> anomaly"instantiate_params: type, ctxt and args mismatch"
-  in inst [] t (List.rev sign,args)
+  let fail () =
+    anomaly "instantiate_params: type, ctxt and args mismatch" in
+  let (rem_args, subs, ty) =
+    Sign.fold_rel_context
+      (fun (_,copt,_) (largs,subs,ty) ->
+        match (copt, largs, kind_of_term ty) with
+          | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t)
+          | (Some b,_,LetIn(_,_,_,t))    -> (largs, (substl subs b)::subs, t)
+	  | _                            -> fail())
+      sign
+      (args,[],t) in
+  if rem_args <> [] then fail();
+  substl subs ty
 
 let full_inductive_instantiate (mispec,params) t =
   instantiate_params t params mispec.mis_mip.mind_params_ctxt
@@ -177,12 +180,16 @@ let get_constructors ((mispec,params) as indf) =
 
 (* Type of case branches *)
 
-let local_rels =
-  let rec relrec acc n = function (* more recent arg in front *)
-    | [] -> acc
-    | (_,None,_)::l -> relrec (mkRel n :: acc) (n+1) l
-    | (_,Some _,_)::l -> relrec acc (n+1) l
-  in relrec [] 1
+let local_rels ctxt =
+  let (rels,_) =
+    Sign.fold_rel_context_reverse
+      (fun (rels,n) (_,copt,_) ->
+        match copt with
+            None   -> (mkRel n :: rels, n+1)
+          | Some _ -> (rels, n+1))
+      ([],1)
+      ctxt in
+  rels
 
 let build_dependent_constructor cs =
   applist
@@ -264,7 +271,7 @@ let is_correct_arity env kelim (c,pj) indf t =
     let create_sort = function 
       | InProp -> mkProp
       | InSet -> mkSet
-      | InType -> mkType (Univ.new_univ ()) in
+      | InType -> mkSort type_0 in
     let listarity = List.map create_sort kelim
 (*    let listarity =
       (List.map (fun s -> make_arity env true indf (create_sort s)) kelim)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index f4d5b5346..d9add1e6f 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -18,7 +18,7 @@ open Environ
 
 exception Induc
 
-(*s Extracting an inductive type from a constructions *)
+(*s Extracting an inductive type from a construction *)
 
 (* [find_m*type env sigma c] coerce [c] to an recursive type (I args).
    [find_rectype], [find_inductive] and [find_coinductive]
diff --git a/kernel/names.mli b/kernel/names.mli
index 3aac8c40b..5a01c2d86 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -8,10 +8,6 @@
 
 (*i $Id$ i*)
 
-(*i*)
-open Pp
-(*i*)
-
 (*s Identifiers *)
 
 type identifier
@@ -19,7 +15,7 @@ type name = Name of identifier | Anonymous
 (* Parsing and printing of identifiers *)
 val string_of_id : identifier -> string
 val id_of_string : string -> identifier
-val pr_id : identifier -> std_ppcmds
+val pr_id : identifier -> Pp.std_ppcmds
 
 (* Identifiers sets and maps *)
 module Idset  : Set.S with type elt = identifier
@@ -38,7 +34,7 @@ val repr_dirpath : dir_path -> module_ident list
 
 (* Printing of directory paths as ["coq_root.module.submodule"] *)
 val string_of_dirpath : dir_path -> string
-val pr_dirpath : dir_path -> std_ppcmds
+val pr_dirpath : dir_path -> Pp.std_ppcmds
 
 
 (*s Section paths are {\em absolute} names *)
@@ -52,7 +48,7 @@ val repr_path : section_path -> dir_path * identifier
 
 (* Parsing and printing of section path as ["coq_root.module.id"] *)
 val string_of_path : section_path -> string
-val pr_sp : section_path -> std_ppcmds
+val pr_sp : section_path -> Pp.std_ppcmds
 
 module Spset  : Set.S with type elt = section_path
 module Sppred : Predicate.S with type elt = section_path
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 10ce90291..4e99446b6 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -290,7 +290,7 @@ let dest_prod env =
 	  decrec (push_rel d env) (Sign.add_rel_decl d m) c0
       | _ -> m,t
   in 
-  decrec env []
+  decrec env Sign.empty_rel_context
 
 (* The same but preserving lets *)
 let dest_prod_assum env = 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index d67b321e9..625833547 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -43,5 +43,5 @@ val conv_leq_vecti : types array conversion_function
 val dest_prod       : env -> types -> Sign.rel_context * types
 val dest_prod_assum : env -> types -> Sign.rel_context * types
 
-val dest_arity : env -> types -> arity
+val dest_arity : env -> types -> Sign.arity
 val is_arity   : env -> types -> bool
diff --git a/kernel/sign.ml b/kernel/sign.ml
index c9da4ab65..61b23ec26 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -12,69 +12,50 @@ open Names
 open Util
 open Term
 
-(* Signatures *)
-
-let add d sign = d::sign
-let map f = List.map (fun (na,c,t) -> (na,option_app f c,type_app f t))
-
-let add_decl (n,t) sign = (n,None,t)::sign
-let add_def (n,c,t) sign = (n,Some c,t)::sign
+(*s Signatures of named hypotheses. Used for section variables and
+    goal assumptions. *)
 
 type named_declaration = identifier * constr option * types
 type named_context = named_declaration list
 
-let add_named_decl = add
-let add_named_assum = add_decl
-let add_named_def = add_def
+let empty_named_context = []
+
+let add_named_decl d sign = d::sign
+
 let rec lookup_named id = function
   | (id',_,_ as decl) :: _ when id=id' -> decl
   | _ :: sign -> lookup_named id sign
   | [] -> raise Not_found
-let empty_named_context = []
+
+let named_context_length = List.length
+
 let pop_named_decl id = function
   | (id',_,_) :: sign -> assert (id = id'); sign
   | [] -> assert false
-let ids_of_named_context = List.map (fun (id,_,_) -> id)
+
 let instance_from_named_context sign =
   let rec inst_rec = function
     | (id,None,_) :: sign -> mkVar id :: inst_rec sign
     | _ :: sign -> inst_rec sign
     | [] -> [] in
   Array.of_list (inst_rec sign)
-let map_named_context = map
-let rec mem_named_context id = function
-  | (id',_,_) :: _ when id=id' -> true
-  | _ :: sign -> mem_named_context id sign
-  | [] -> false
+
 let fold_named_context = List.fold_right
 let fold_named_context_reverse = List.fold_left
-let fold_named_context_both_sides = list_fold_right_and_left
-let it_named_context_quantifier f = List.fold_left (fun c d -> f d c)
-
-let it_mkNamedProd_or_LetIn   =
-  List.fold_left (fun c d -> mkNamedProd_or_LetIn d c)
-let it_mkNamedLambda_or_LetIn =
-  List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c)
 
 (*s Signatures of ordered section variables *)
 type section_context = named_context
 
 (*s Signatures of ordered optionally named variables, intended to be
-   accessed by de Bruijn indices *)
+   accessed by de Bruijn indices (to represent bound variables) *)
 
 type rel_declaration = name * constr option * types
 type rel_context = rel_declaration list
-type rev_rel_context = rel_declaration list
 
-let fold_rel_context = List.fold_right
-let fold_rel_context_reverse = List.fold_left
+let empty_rel_context = []
 
-let it_mkProd_or_LetIn   = List.fold_left (fun c d -> mkProd_or_LetIn d c)
-let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
+let add_rel_decl d ctxt = d::ctxt
 
-let add_rel_decl = add
-let add_rel_assum = add_decl
-let add_rel_def = add_def
 let lookup_rel n sign =
   let rec lookrec = function
     | (1, decl :: _) -> decl
@@ -82,38 +63,14 @@ let lookup_rel n sign =
     | (_, [])        -> raise Not_found
   in 
   lookrec (n,sign)
-let rec lookup_rel_id id sign = 
-  let rec lookrec = function
-    | (n, (Anonymous,_,_)::l) -> lookrec (n+1,l)
-    | (n, (Name id',_,t)::l)  -> if id' = id then (n,t) else lookrec (n+1,l)
-    | (_, [])                 -> raise Not_found
-  in 
-  lookrec (1,sign)
-let empty_rel_context = []
+
 let rel_context_length = List.length
-let lift_rel_context n sign =
-  let rec liftrec k = function
-    | (na,c,t)::sign ->
-	(na,option_app (liftn n k) c,type_app (liftn n k) t)
-	::(liftrec (k-1) sign)
-    | [] -> []
-  in
-  liftrec (rel_context_length sign) sign
-let lift_rev_rel_context n sign =
-  let rec liftrec k = function
-    | (na,c,t)::sign ->
-	(na,option_app (liftn n k) c,type_app (liftn n k) t)
-	::(liftrec (k+1) sign)
-    | [] -> []
-  in
-  liftrec 1 sign
-let concat_rel_context = (@)
-let ids_of_rel_context sign =
-  List.fold_right
-    (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l)
-    sign []
-let names_of_rel_context = List.map (fun (na,_,_) -> na)
-let map_rel_context = map
+
+let fold_rel_context = List.fold_right
+let fold_rel_context_reverse = List.fold_left
+
+(* Push named declarations on top of a rel context *)
+(* Bizarre. Should be avoided. *)
 let push_named_to_rel_context hyps ctxt =
   let rec push = function
     | (id,b,t) :: l ->
@@ -129,47 +86,54 @@ let push_named_to_rel_context hyps ctxt =
 	(n+1), d::ctxt
     | [] -> 1, hyps in
   snd (subst ctxt)
-let reverse_rel_context = List.rev
-
-let instantiate_sign sign args =
-  let rec instrec = function
-    | ((id,None,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args))
-    | ((id,Some c,_) :: sign, args)  -> instrec (sign,args)
-    | ([],[])                        -> []
-    | ([],_) | (_,[]) ->
-    anomaly "Signature and its instance do not match"
-  in 
-  instrec (sign,Array.to_list args)
-
-(*************************)
-(*   Names environments  *)
-(*************************)
-type names_context = name list
-let add_name n nl = n::nl
-let lookup_name_of_rel p names =
-  try List.nth names (p-1)
-  with Invalid_argument _ | Failure _ -> raise Not_found
-let rec lookup_rel_of_name id names = 
-  let rec lookrec n = function
-    | Anonymous :: l  -> lookrec (n+1) l
-    | (Name id') :: l -> if id' = id then n else lookrec (n+1) l
-    | []            -> raise Not_found
-  in 
-  lookrec 1 names
-let empty_names_context = []
+
+
+(*********************************)
+(*       Term constructors       *)
+(*********************************)
+
+let it_mkNamedProd_or_LetIn   =
+  List.fold_left (fun c d -> mkNamedProd_or_LetIn d c)
+let it_mkNamedLambda_or_LetIn =
+  List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c)
+let it_mkProd_or_LetIn   = List.fold_left (fun c d -> mkProd_or_LetIn d c)
+let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
 
 (*********************************)
 (*       Term destructors        *)
 (*********************************)
 
+type arity = rel_context * sorts
+
+(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
+   ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
+let destArity = 
+  let rec prodec_rec l c =
+    match kind_of_term c with
+    | Prod (x,t,c)    -> prodec_rec ((x,None,t)::l) c
+    | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c
+    | Cast (c,_)      -> prodec_rec l c
+    | Sort s          -> l,s
+    | _               -> anomaly "destArity: not an arity"
+  in 
+  prodec_rec [] 
+
+let rec isArity c =
+  match kind_of_term c with
+  | Prod (_,_,c)    -> isArity c
+  | LetIn (_,b,_,c) -> isArity (subst1 b c)
+  | Cast (c,_)      -> isArity c
+  | Sort _          -> true
+  | _               -> false
+
 (* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
    ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
 let decompose_prod_assum = 
   let rec prodec_rec l c =
     match kind_of_term c with
-    | Prod (x,t,c)  -> prodec_rec (add_rel_assum (x,t) l) c
-    | LetIn (x,b,t,c) -> prodec_rec (add_rel_def (x,b,t) l) c
-    | Cast (c,_)    -> prodec_rec l c
+    | Prod (x,t,c)    -> prodec_rec (add_rel_decl (x,None,t) l) c
+    | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) c
+    | Cast (c,_)      -> prodec_rec l c
     | _               -> l,c
   in 
   prodec_rec empty_rel_context
@@ -179,10 +143,10 @@ let decompose_prod_assum =
 let decompose_lam_assum = 
   let rec lamdec_rec l c =
     match kind_of_term c with
-    | Lambda (x,t,c) -> lamdec_rec (add_rel_assum (x,t) l) c
-    | LetIn (x,b,t,c) -> lamdec_rec (add_rel_def (x,b,t) l) c
-    | Cast (c,_)     -> lamdec_rec l c
-    | _                -> l,c
+    | Lambda (x,t,c)  -> lamdec_rec (add_rel_decl (x,None,t) l) c
+    | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) c
+    | Cast (c,_)      -> lamdec_rec l c
+    | _               -> l,c
   in 
   lamdec_rec empty_rel_context
 
@@ -194,10 +158,9 @@ let decompose_prod_n_assum n =
   let rec prodec_rec l n c = 
     if n=0 then l,c 
     else match kind_of_term c with 
-    | Prod (x,t,c) -> prodec_rec (add_rel_assum(x,t) l) (n-1) c
-    | LetIn (x,b,t,c) ->
-	prodec_rec (add_rel_def (x,b,t) l) (n-1) c
-    | Cast (c,_)   -> prodec_rec l n c
+    | Prod (x,t,c)    -> prodec_rec (add_rel_decl (x,None,t) l) (n-1) c
+    | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
+    | Cast (c,_)      -> prodec_rec l n c
     | c -> error "decompose_prod_n_assum: not enough assumptions"
   in 
   prodec_rec empty_rel_context n 
@@ -210,10 +173,9 @@ let decompose_lam_n_assum n =
   let rec lamdec_rec l n c = 
     if n=0 then l,c 
     else match kind_of_term c with 
-    | Lambda (x,t,c) -> lamdec_rec (add_rel_assum (x,t) l) (n-1) c
-    | LetIn (x,b,t,c) ->
-	lamdec_rec (add_rel_def (x,b,t) l) (n-1) c
-    | Cast (c,_)     -> lamdec_rec l n c
+    | Lambda (x,t,c)  -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c
+    | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
+    | Cast (c,_)      -> lamdec_rec l n c
     | c -> error "decompose_lam_n_assum: not enough abstractions"
   in 
   lamdec_rec empty_rel_context n 
diff --git a/kernel/sign.mli b/kernel/sign.mli
index d834e263a..61e97d9eb 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -23,18 +23,17 @@ val add_named_decl : named_declaration -> named_context -> named_context
 val pop_named_decl : identifier -> named_context -> named_context
 
 val lookup_named : identifier -> named_context -> named_declaration
+val named_context_length : named_context -> int
 
 (*s Recurrence on [named_context]: older declarations processed first *)
 val fold_named_context :
-  (named_declaration -> 'a -> 'a) -> named_context -> 'a -> 'a
+  (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a
 (* newer declarations first *)
 val fold_named_context_reverse :
-  ('a -> named_declaration -> 'a) -> 'a -> named_context -> 'a
+  ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a
 
 (*s Section-related auxiliary functions *)
 val instance_from_named_context : named_context -> constr array
-val instantiate_sign :
-  named_context -> constr array -> (identifier * constr) list
 
 (*s Signatures of ordered optionally named variables, intended to be
    accessed by de Bruijn indices *)
@@ -52,10 +51,10 @@ val push_named_to_rel_context : named_context -> rel_context -> rel_context
 
 (*s Recurrence on [rel_context]: older declarations processed first *)
 val fold_rel_context :
-  (rel_declaration -> 'a -> 'a) -> rel_context -> 'a -> 'a
+  (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
 (* newer declarations first *)
 val fold_rel_context_reverse :
-  ('a -> rel_declaration -> 'a) -> 'a -> rel_context -> 'a
+  ('a -> rel_declaration -> 'a) -> init:'a -> rel_context -> 'a
 
 (*s Term constructors *)
 
@@ -67,6 +66,11 @@ val it_mkProd_or_LetIn : constr -> rel_context -> constr
 
 (*s Term destructors *)
 
+(* Destructs a term of the form $(x_1:T_1)..(x_n:T_n)s$ into the pair *)
+type arity = rel_context * sorts
+val destArity : constr -> arity
+val isArity : constr -> bool
+
 (* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ including letins
    into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a
    product nor a let. *)
diff --git a/kernel/term.ml b/kernel/term.ml
index 652c4d3c3..90614e7da 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -47,11 +47,6 @@ let mk_Prop = Prop Null
 
 type sorts_family = InProp | InSet | InType
 
-let new_sort_in_family = function 
-  | InProp -> mk_Prop
-  | InSet -> mk_Set
-  | InType -> Type (Univ.new_univ ())
-
 let family_of_sort = function
   | Prop Null -> InProp
   | Prop Pos -> InSet
@@ -907,7 +902,6 @@ let mkSort   = function
 
 let prop = mk_Prop
 and spec = mk_Set
-and types = Type implicit_univ (* For eliminations *)
 and type_0 = Type prop_univ
 
 (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *)
@@ -1031,7 +1025,7 @@ let mkFix = mkFix
 let mkCoFix = mkCoFix
 
 (* Construct an implicit *)
-let implicit_sort = Type implicit_univ
+let implicit_sort = Type (make_univ(make_dirpath[id_of_string"implicit"],0))
 let mkImplicit = mkSort implicit_sort
 
 let rec strip_outer_cast c = match kind_of_term c with
@@ -1124,28 +1118,6 @@ let prod_applist t nL = List.fold_left prod_app t nL
 (* Other term destructors        *)
 (*********************************)
 
-type arity = rel_declaration list * sorts
-
-(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
-   ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
-let destArity = 
-  let rec prodec_rec l c =
-    match kind_of_term c with
-    | Prod (x,t,c) -> prodec_rec ((x,None,t)::l) c
-    | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c
-    | Cast (c,_)   -> prodec_rec l c
-    | Sort s       -> l,s
-    | _              -> anomaly "destArity: not an arity"
-  in 
-  prodec_rec [] 
-
-let rec isArity c =
-  match kind_of_term c with
-  | Prod (_,_,c) -> isArity c
-  | Cast (c,_)   -> isArity c
-  | Sort _       -> true
-  | _ -> false
-
 (* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
    ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
 let decompose_prod = 
diff --git a/kernel/term.mli b/kernel/term.mli
index 0ce4f3d4a..66cc90fb3 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -29,7 +29,6 @@ val type_0  : sorts
 type sorts_family = InProp | InSet | InType
 
 val family_of_sort : sorts -> sorts_family
-val new_sort_in_family : sorts_family -> sorts
 
 (*s Useful types *)
 
@@ -344,11 +343,6 @@ val prod_applist : constr -> constr list -> constr
 
 (*s Other term destructors. *)
 
-(* Destructs a term of the form $(x_1:T_1)..(x_n:T_n)s$ into the pair *)
-type arity = rel_declaration list * sorts
-val destArity : constr -> arity
-val isArity : constr -> bool
-
 (* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ into the pair
    $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a product.
    It includes also local definitions *)
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 169df5904..b057ff839 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -36,6 +36,7 @@ type guard_error =
 
 type type_error =
   | UnboundRel of int
+  | UnboundVar of variable
   | NotAType of unsafe_judgment
   | BadAssumption of unsafe_judgment
   | ReferenceVariables of constr
@@ -47,12 +48,12 @@ type type_error =
   | IllFormedBranch of constr * int * constr * constr
   | Generalization of (name * types) * unsafe_judgment
   | ActualType of unsafe_judgment * types
-  | CantApplyBadType of (int * constr * constr)
-      * unsafe_judgment * unsafe_judgment array
+  | CantApplyBadType of
+      (int * constr * constr) * unsafe_judgment * unsafe_judgment array
   | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
   | IllFormedRecBody of guard_error * name array * int * constr array
-  | IllTypedRecBody of int * name array * unsafe_judgment array 
-      * types array
+  | IllTypedRecBody of
+      int * name array * unsafe_judgment array * types array
 
 exception TypeError of env * type_error
 
@@ -62,6 +63,9 @@ let nfj {uj_val=c;uj_type=ct} =
 let error_unbound_rel env n =
   raise (TypeError (env, UnboundRel n))
 
+let error_unbound_var env v =
+  raise (TypeError (env, UnboundVar v))
+
 let error_not_type env j =
   raise (TypeError (env, NotAType j))
 
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index c342ce892..3ffb585c5 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -11,7 +11,6 @@
 (*i*)
 open Names
 open Term
-open Sign
 open Environ
 (*i*)
 
@@ -39,6 +38,7 @@ type guard_error =
 
 type type_error =
   | UnboundRel of int
+  | UnboundVar of variable
   | NotAType of unsafe_judgment
   | BadAssumption of unsafe_judgment
   | ReferenceVariables of constr
@@ -50,17 +50,19 @@ type type_error =
   | IllFormedBranch of constr * int * constr * constr
   | Generalization of (name * types) * unsafe_judgment
   | ActualType of unsafe_judgment * types
-  | CantApplyBadType of (int * constr * constr)
-      * unsafe_judgment * unsafe_judgment array
+  | CantApplyBadType of
+      (int * constr * constr) * unsafe_judgment * unsafe_judgment array
   | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
   | IllFormedRecBody of guard_error * name array * int * constr array
-  | IllTypedRecBody of int * name array * unsafe_judgment array 
-      * types array
+  | IllTypedRecBody of
+      int * name array * unsafe_judgment array * types array
 
 exception TypeError of env * type_error
 
 val error_unbound_rel : env -> int -> 'a
 
+val error_unbound_var : env -> variable -> 'a
+
 val error_not_type : env -> unsafe_judgment -> 'a
 
 val error_assumption : env -> unsafe_judgment -> 'a
@@ -71,20 +73,15 @@ val error_elim_arity :
   env -> inductive -> constr list -> constr 
     -> unsafe_judgment -> (constr * constr * string) option -> 'a
 
-val error_case_not_inductive : 
-  env -> unsafe_judgment -> 'a
+val error_case_not_inductive : env -> unsafe_judgment -> 'a
 
-val error_number_branches : 
-  env -> unsafe_judgment -> int -> 'a
+val error_number_branches : env -> unsafe_judgment -> int -> 'a
 
-val error_ill_formed_branch :
-  env -> constr -> int -> constr -> constr -> 'a
+val error_ill_formed_branch : env -> constr -> int -> constr -> constr -> 'a
 
-val error_generalization :
-  env -> name * types -> unsafe_judgment -> 'a
+val error_generalization : env -> name * types -> unsafe_judgment -> 'a
 
-val error_actual_type :
-  env -> unsafe_judgment -> types -> 'a
+val error_actual_type : env -> unsafe_judgment -> types -> 'a
 
 val error_cant_apply_not_functional : 
   env -> unsafe_judgment -> unsafe_judgment array -> 'a
@@ -97,6 +94,5 @@ val error_ill_formed_rec_body :
   env -> guard_error -> name array -> int -> constr array -> 'a
 
 val error_ill_typed_rec_body  :
-  env -> int -> name array -> unsafe_judgment array 
-    -> types array -> 'a
+  env -> int -> name array -> unsafe_judgment array -> types array -> 'a
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index e99673fe1..603e909bd 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -62,10 +62,9 @@ let judge_of_prop_contents = function
 (* Type of Type(i). *)
 
 let judge_of_type u =
-  let (uu,c) = super u in
+  let uu = super u in
   { uj_val = mkType u;
-    uj_type = mkType uu },
-  c
+    uj_type = mkType uu }
 
 (*s Type of a de Bruijn index. *)
 	  
@@ -83,6 +82,14 @@ let judge_of_relative env n =
   Profile.profile2 relativekey judge_of_relative env n;;
 *)
 
+(* Type of variables *)
+let judge_of_variable env id =
+  try
+    let (_,_,ty) = lookup_named id env in
+    make_judge (mkVar id) ty
+  with Not_found -> 
+    error_unbound_var env id
+
 (* Management of context of variables. *)
 
 (* Checks if a context of variable can be instanciated by the
@@ -116,14 +123,6 @@ let check_hyps id env hyps =
 *)
 (* Instantiation of terms on real arguments. *)
 
-(* Type of variables *)
-let judge_of_variable env id =
-  try
-    let (_,_,ty) = lookup_named id env in
-    make_judge (mkVar id) ty
-  with Not_found -> 
-    error ("execute: variable " ^ (string_of_id id) ^ " not defined")
-
 (* Type of constants *)
 let judge_of_constant env cst =
   let constr = mkConst cst in
@@ -198,16 +197,14 @@ let judge_of_apply env nocheck funj argjl
 
 (* Type of product *)
 
-let sort_of_product domsort rangsort g =
-  match rangsort with
+let sort_of_product domsort rangsort =
+  match (domsort, 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)
+    | (_,       Prop _)  -> rangsort
+    (* Product rule (Prop,Type_i,Type_i) *)
+    | (Prop _,  Type _)  -> rangsort
+    (* Product rule (Type_i,Type_i,Type_i) *) 
+    | (Type u1, Type u2) -> Type (sup u1 u2)
 
 (* [judge_of_product env name (typ1,s1) (typ2,s2)] implements the rule
 
@@ -218,10 +215,9 @@ let sort_of_product domsort rangsort g =
   where j.uj_type is convertible to a sort s2
 *)
 let judge_of_product env name t1 t2 =
-  let (s,g) = sort_of_product t1.utj_type t2.utj_type (universes env) in
+  let s = sort_of_product t1.utj_type t2.utj_type in
   { uj_val = mkProd (name, t1.utj_val, t2.utj_val);
-    uj_type = mkSort s },
-  g
+    uj_type = mkSort s }
 
 (* Type of a type cast *)
 
@@ -339,7 +335,7 @@ let rec execute env cstr cu =
 	(judge_of_prop_contents c, cu)
 
     | Sort (Type u) ->
-	univ_combinator cu (judge_of_type u)
+	(judge_of_type u, cu)
 
     | Rel n -> 
 	(judge_of_relative env n, cu)
@@ -367,8 +363,7 @@ let rec execute env cstr cu =
         let (varj,cu1) = execute_type env c1 cu in
 	let env1 = push_rel (name,None,varj.utj_val) env in
         let (varj',cu2) = execute_type env1 c2 cu1 in
-	univ_combinator cu2
-          (judge_of_product env name varj varj')
+	(judge_of_product env name varj varj', cu2)
 
     | LetIn (name,c1,c2,c3) ->
         let (j1,cu1) = execute env c1 cu in
@@ -479,6 +474,6 @@ let infer_local_decls env decls =
   | (id, d) :: l -> 
       let env, l, cst1 = inferec env l in
       let d, cst2 = infer_local_decl env id d in
-      push_rel d env, d :: l, Constraint.union cst1 cst2
-  | [] -> env, [], Constraint.empty in
+      push_rel d env, add_rel_decl d l, Constraint.union cst1 cst2
+  | [] -> env, empty_rel_context, Constraint.empty in
   inferec env decls
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 1605328cb..2a678cd49 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -13,7 +13,6 @@ open Names
 open Univ
 open Term
 open Environ
-open Inductive
 (*i*)
 
 (*s Typing functions (not yet tagged as safe) *)
@@ -40,13 +39,13 @@ val type_judgment          :  env -> unsafe_judgment -> unsafe_type_judgment
 
 (*s Type of sorts. *)
 val judge_of_prop_contents : contents -> unsafe_judgment
-val judge_of_type          : universe -> unsafe_judgment * constraints
+val judge_of_type          : universe -> unsafe_judgment
 
 (*s Type of a bound variable. *)
 val judge_of_relative : env -> int -> unsafe_judgment
 
 (*s Type of variables *)
-val judge_of_variable : env -> identifier -> unsafe_judgment
+val judge_of_variable : env -> variable -> unsafe_judgment
 
 (*s type of a constant *)
 val judge_of_constant : env -> constant -> unsafe_judgment
@@ -64,7 +63,7 @@ val judge_of_abstraction :
 (*s Type of a product. *)
 val judge_of_product :
   env -> name -> unsafe_type_judgment -> unsafe_type_judgment 
-    -> unsafe_judgment * constraints
+    -> unsafe_judgment
 
 (* s Type of a let in. *)
 val judge_of_letin :
diff --git a/kernel/univ.ml b/kernel/univ.ml
index b55b3ca6f..99dd2ee36 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -23,23 +23,23 @@
 open Pp
 open Util
 
-type universe_level = { u_mod : Names.dir_path; u_num : int }
+type universe_level =
+    { u_mod : Names.dir_path;
+      u_num : int }
 
 type universe =
   | Variable of universe_level
   | Max of universe_level list * universe_level list
-
-let universe_ord x y =
-  let c = x.u_num - y.u_num in
-  if c <> 0 then c else compare x.u_mod y.u_mod
   
 module UniverseOrdered = struct
   type t = universe_level
-  let compare = universe_ord
+  let compare = Pervasives.compare
 end
 
-let string_of_univ_level u = 
-  (Names.string_of_dirpath u.u_mod)^"."^(string_of_int u.u_num)
+let string_of_univ_level u =
+  Names.string_of_dirpath u.u_mod^"."^string_of_int u.u_num
+
+let make_univ (m,n) = Variable { u_mod=m; u_num=n }
 
 let string_of_univ = function
   | Variable u -> string_of_univ_level u
@@ -49,8 +49,7 @@ let string_of_univ = function
 	 ((List.map string_of_univ_level gel)@
 	  (List.map (fun u -> "("^(string_of_univ_level u)^")+1") gtl)))^")"
 
-let pr_uni_level u =
-  [< 'sTR (Names.string_of_dirpath u.u_mod) ; 'sTR"." ; 'iNT u.u_num >]
+let pr_uni_level u = [< 'sTR (string_of_univ_level u) >]
 
 let pr_uni = function
   | Variable u -> pr_uni_level u
@@ -62,20 +61,26 @@ let pr_uni = function
 	   (fun x -> [< 'sTR "("; pr_uni_level x; 'sTR")+1" >]) gtl;
 	 'sTR ")" >]
 
-let implicit_univ =
-  Variable 
-    { u_mod = Names.make_dirpath [Names.id_of_string "implicit_univ"];
-      u_num = 0 }
-
-let current_module = ref (Names.make_dirpath[Names.id_of_string"Top"])
-
-let set_module m = current_module := m
+(* 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 = function
+  | Variable u -> Max ([],[u])
+  | Max _ ->
+      anomaly ("Cannot take the successor of a non variable universes:\n"^
+       "you are probably typing a type already known to be the type\n"^
+       "of a user-provided term; if you really need this, please report")
 
-let new_univ = 
-  let univ_gen = ref 0 in
-  (fun sp ->
-     incr univ_gen; 
-     Variable { u_mod = !current_module; u_num = !univ_gen })
+(* 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. *)
+let sup u v = 
+  match u,v with
+    | Variable u, Variable v -> Max ((if u = v then [u] else [u;v]),[])
+    | Variable u, Max (gel,gtl) -> Max (list_add_set u gel,gtl)
+    | Max (gel,gtl), Variable v -> Max (list_add_set v gel,gtl)
+    | Max (gel,gtl), Max (gel',gtl') ->
+	Max (list_union gel gel',list_union gtl gtl')
 
 (* Comparison on this type is pointer equality *)
 type canonical_arc =
@@ -386,28 +391,6 @@ let enforce_eq u v c =
 let merge_constraints c g =
   Constraint.fold enforce_constraint 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 = function
-  | Variable u -> Max ([],[u]), Constraint.empty
-  | Max _ ->
-      anomaly ("Cannot take the successor of a non variable universes:\n"^
-       "you are probably typing a type already known to be the type\n"^
-       "of a user-provided term; if you really need this, please report")
-
-(* 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. *)
-let sup u v g = 
-  (match u,v with
-    | Variable u, Variable v -> Max ((if u = v then [u] else [u;v]),[])
-    | Variable u, Max (gel,gtl) -> Max (list_add_set u gel,gtl)
-    | Max (gel,gtl), Variable v -> Max (list_add_set v gel,gtl)
-    | Max (gel,gtl), Max (gel',gtl') ->
-	Max (list_union gel gel',list_union gtl gtl')),
-  Constraint.empty
-
 (* Pretty-printing *)
 
 let num_universes g =
@@ -462,7 +445,7 @@ module Huniv =
     struct
       type t = universe
       type u = Names.dir_path -> Names.dir_path
-      let hash_aux hdir {u_mod=sp; u_num=n} = {u_mod = hdir sp; u_num = n}
+      let hash_aux hdir u = { u with u_mod=hdir u.u_mod }
       let hash_sub hdir = function
 	| Variable u -> Variable (hash_aux hdir u)
 	| Max (gel,gtl) ->
@@ -477,6 +460,6 @@ module Huniv =
     end)
 
 let hcons1_univ u =
-  let _,hdir,_,_,_ = Names.hcons_names () in
+  let _,hdir,_,_,_ = Names.hcons_names() in
   Hashcons.simple_hcons Huniv.f hdir u
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 97dd6bdef..0da9b79df 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -12,18 +12,19 @@
 
 type universe
 
-val implicit_univ : universe
-
 val prop_univ : universe
+val make_univ : Names.dir_path * int -> universe
 
-val set_module : Names.dir_path -> unit
-
-val new_univ : unit -> universe
+(* The type of a universe *)
+val super : universe -> universe
+(* The max of 2 universes *)
+val sup   : universe -> universe -> universe
 
 (*s Graphs of universes. *)
 
 type universes
 
+(* The empty graph of universes *)
 val initial_universes : universes
 
 (*s Constraints. *)
@@ -37,10 +38,6 @@ type constraint_function = universe -> universe -> constraints -> constraints
 val enforce_geq : constraint_function
 val enforce_eq : constraint_function
 
-val super : 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