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

41 files changed, 394 insertions, 555 deletions

diff --git a/.depend b/.depend
index bbdc9be1b..d492d8a8d 100644
--- a/.depend
+++ b/.depend
@@ -19,10 +19,9 @@ kernel/safe_typing.cmi: kernel/cooking.cmi kernel/declarations.cmi \
     kernel/univ.cmi 
 kernel/sign.cmi: kernel/names.cmi kernel/term.cmi 
 kernel/term.cmi: kernel/names.cmi kernel/univ.cmi 
-kernel/type_errors.cmi: kernel/environ.cmi kernel/names.cmi kernel/sign.cmi \
-    kernel/term.cmi 
-kernel/typeops.cmi: kernel/environ.cmi kernel/inductive.cmi kernel/names.cmi \
-    kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
+kernel/type_errors.cmi: kernel/environ.cmi kernel/names.cmi kernel/term.cmi 
+kernel/typeops.cmi: kernel/environ.cmi kernel/names.cmi kernel/sign.cmi \
+    kernel/term.cmi kernel/univ.cmi 
 kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
 library/declare.cmi: kernel/cooking.cmi kernel/declarations.cmi \
@@ -31,11 +30,12 @@ library/declare.cmi: kernel/cooking.cmi kernel/declarations.cmi \
     kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
 library/global.cmi: kernel/cooking.cmi kernel/declarations.cmi \
     kernel/environ.cmi kernel/indtypes.cmi kernel/names.cmi \
-    kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
+    library/nametab.cmi kernel/safe_typing.cmi kernel/sign.cmi \
+    kernel/term.cmi kernel/univ.cmi 
 library/goptions.cmi: kernel/names.cmi library/nametab.cmi lib/pp.cmi \
     kernel/term.cmi 
-library/impargs.cmi: kernel/environ.cmi kernel/inductive.cmi kernel/names.cmi \
-    library/nametab.cmi kernel/term.cmi 
+library/impargs.cmi: kernel/environ.cmi kernel/names.cmi library/nametab.cmi \
+    kernel/term.cmi 
 library/lib.cmi: library/libobject.cmi kernel/names.cmi library/summary.cmi 
 library/libobject.cmi: kernel/names.cmi 
 library/library.cmi: library/lib.cmi library/libobject.cmi kernel/names.cmi \
@@ -68,9 +68,9 @@ parsing/g_minicoq.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
 parsing/g_zsyntax.cmi: parsing/coqast.cmi 
 parsing/pcoq.cmi: parsing/coqast.cmi 
 parsing/prettyp.cmi: pretyping/classops.cmi kernel/environ.cmi \
-    kernel/inductive.cmi library/lib.cmi kernel/names.cmi library/nametab.cmi \
-    lib/pp.cmi pretyping/reductionops.cmi kernel/safe_typing.cmi \
-    kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi 
+    library/lib.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
+    pretyping/reductionops.cmi kernel/safe_typing.cmi kernel/sign.cmi \
+    kernel/term.cmi pretyping/termops.cmi 
 parsing/printer.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \
     library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \
     pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \
@@ -131,7 +131,7 @@ pretyping/tacred.cmi: kernel/closure.cmi kernel/environ.cmi pretyping/evd.cmi \
     kernel/names.cmi pretyping/reductionops.cmi kernel/term.cmi 
 pretyping/termops.cmi: kernel/environ.cmi kernel/names.cmi \
     library/nametab.cmi lib/pp.cmi kernel/sign.cmi kernel/term.cmi \
-    lib/util.cmi 
+    kernel/univ.cmi lib/util.cmi 
 pretyping/typing.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/term.cmi 
 proofs/clenv.cmi: kernel/environ.cmi proofs/evar_refiner.cmi \
     pretyping/evd.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \
@@ -143,8 +143,8 @@ proofs/evar_refiner.cmi: parsing/coqast.cmi kernel/environ.cmi \
 proofs/logic.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \
     lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi kernel/term.cmi 
 proofs/pfedit.cmi: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \
-    kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi kernel/safe_typing.cmi \
-    kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi 
+    pretyping/evd.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \
+    kernel/safe_typing.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi 
 proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi \
     pretyping/evd.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \
     kernel/sign.cmi lib/stamps.cmi kernel/term.cmi lib/util.cmi 
@@ -152,11 +152,11 @@ proofs/proof_type.cmi: parsing/coqast.cmi kernel/environ.cmi \
     pretyping/evd.cmi kernel/names.cmi library/nametab.cmi \
     pretyping/pretyping.cmi lib/stamps.cmi pretyping/tacred.cmi \
     kernel/term.cmi lib/util.cmi 
-proofs/refiner.cmi: lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
-    kernel/sign.cmi kernel/term.cmi 
+proofs/refiner.cmi: pretyping/evd.cmi lib/pp.cmi proofs/proof_trees.cmi \
+    proofs/proof_type.cmi kernel/sign.cmi kernel/term.cmi 
 proofs/tacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/environ.cmi \
-    kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacmach.cmi \
-    proofs/tactic_debug.cmi kernel/term.cmi 
+    pretyping/evd.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \
+    proofs/tacmach.cmi proofs/tactic_debug.cmi kernel/term.cmi 
 proofs/tacmach.cmi: kernel/closure.cmi parsing/coqast.cmi kernel/environ.cmi \
     pretyping/evd.cmi kernel/names.cmi lib/pp.cmi pretyping/pretyping.cmi \
     proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \
@@ -206,8 +206,8 @@ tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/environ.cmi \
 toplevel/class.cmi: pretyping/classops.cmi library/declare.cmi \
     kernel/names.cmi library/nametab.cmi kernel/term.cmi 
 toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi \
-    kernel/environ.cmi kernel/indtypes.cmi library/library.cmi \
-    kernel/names.cmi library/nametab.cmi proofs/proof_type.cmi \
+    kernel/environ.cmi pretyping/evd.cmi kernel/indtypes.cmi \
+    library/library.cmi kernel/names.cmi library/nametab.cmi \
     pretyping/tacred.cmi kernel/term.cmi 
 toplevel/coqinit.cmi: kernel/names.cmi 
 toplevel/discharge.cmi: kernel/names.cmi 
@@ -226,8 +226,8 @@ toplevel/recordobj.cmi: library/nametab.cmi
 toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
     kernel/term.cmi 
 toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi 
-toplevel/vernacentries.cmi: kernel/environ.cmi kernel/names.cmi \
-    proofs/proof_type.cmi kernel/term.cmi toplevel/vernacinterp.cmi 
+toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \
+    kernel/names.cmi kernel/term.cmi toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     library/nametab.cmi proofs/proof_type.cmi 
 toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi 
@@ -455,11 +455,11 @@ library/declare.cmx: kernel/cooking.cmx kernel/declarations.cmx \
     kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx kernel/univ.cmx \
     lib/util.cmx library/declare.cmi 
 library/global.cmo: kernel/environ.cmi kernel/inductive.cmi kernel/names.cmi \
-    kernel/safe_typing.cmi kernel/sign.cmi library/summary.cmi \
-    kernel/term.cmi lib/util.cmi library/global.cmi 
+    library/nametab.cmi kernel/safe_typing.cmi kernel/sign.cmi \
+    library/summary.cmi kernel/term.cmi lib/util.cmi library/global.cmi 
 library/global.cmx: kernel/environ.cmx kernel/inductive.cmx kernel/names.cmx \
-    kernel/safe_typing.cmx kernel/sign.cmx library/summary.cmx \
-    kernel/term.cmx lib/util.cmx library/global.cmi 
+    library/nametab.cmx kernel/safe_typing.cmx kernel/sign.cmx \
+    library/summary.cmx kernel/term.cmx lib/util.cmx library/global.cmi 
 library/goptions.cmo: library/global.cmi library/lib.cmi \
     library/libobject.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
     library/summary.cmi kernel/term.cmi lib/util.cmi library/goptions.cmi 
@@ -477,11 +477,11 @@ library/impargs.cmx: kernel/declarations.cmx kernel/environ.cmx \
     kernel/reduction.cmx library/summary.cmx kernel/term.cmx lib/util.cmx \
     library/impargs.cmi 
 library/lib.cmo: library/libobject.cmi library/nameops.cmi kernel/names.cmi \
-    library/nametab.cmi lib/pp.cmi library/summary.cmi kernel/univ.cmi \
-    lib/util.cmi library/lib.cmi 
+    library/nametab.cmi lib/pp.cmi library/summary.cmi lib/util.cmi \
+    library/lib.cmi 
 library/lib.cmx: library/libobject.cmx library/nameops.cmx kernel/names.cmx \
-    library/nametab.cmx lib/pp.cmx library/summary.cmx kernel/univ.cmx \
-    lib/util.cmx library/lib.cmi 
+    library/nametab.cmx lib/pp.cmx library/summary.cmx lib/util.cmx \
+    library/lib.cmi 
 library/libobject.cmo: lib/dyn.cmi kernel/names.cmi lib/util.cmi \
     library/libobject.cmi 
 library/libobject.cmx: lib/dyn.cmx kernel/names.cmx lib/util.cmx \
@@ -715,13 +715,15 @@ pretyping/cbv.cmx: kernel/closure.cmx kernel/declarations.cmx \
 pretyping/classops.cmo: library/declare.cmi kernel/environ.cmi \
     library/global.cmi library/lib.cmi library/libobject.cmi \
     library/library.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
-    lib/pp.cmi pretyping/rawterm.cmi library/summary.cmi pretyping/tacred.cmi \
-    kernel/term.cmi pretyping/termops.cmi lib/util.cmi pretyping/classops.cmi 
+    lib/pp.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \
+    library/summary.cmi pretyping/tacred.cmi kernel/term.cmi \
+    pretyping/termops.cmi lib/util.cmi pretyping/classops.cmi 
 pretyping/classops.cmx: library/declare.cmx kernel/environ.cmx \
     library/global.cmx library/lib.cmx library/libobject.cmx \
     library/library.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
-    lib/pp.cmx pretyping/rawterm.cmx library/summary.cmx pretyping/tacred.cmx \
-    kernel/term.cmx pretyping/termops.cmx lib/util.cmx pretyping/classops.cmi 
+    lib/pp.cmx pretyping/rawterm.cmx pretyping/reductionops.cmx \
+    library/summary.cmx pretyping/tacred.cmx kernel/term.cmx \
+    pretyping/termops.cmx lib/util.cmx pretyping/classops.cmi 
 pretyping/coercion.cmo: pretyping/classops.cmi kernel/environ.cmi \
     pretyping/evarconv.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
     kernel/names.cmi pretyping/pretype_errors.cmi pretyping/rawterm.cmi \
@@ -858,13 +860,15 @@ pretyping/recordops.cmx: pretyping/classops.cmx library/lib.cmx \
     pretyping/recordops.cmi 
 pretyping/reductionops.cmo: kernel/closure.cmi kernel/declarations.cmi \
     kernel/environ.cmi kernel/esubst.cmi pretyping/evd.cmi \
-    pretyping/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
-    kernel/term.cmi pretyping/termops.cmi kernel/univ.cmi lib/util.cmi \
+    pretyping/instantiate.cmi kernel/names.cmi lib/pp.cmi \
+    kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
+    pretyping/termops.cmi kernel/univ.cmi lib/util.cmi \
     pretyping/reductionops.cmi 
 pretyping/reductionops.cmx: kernel/closure.cmx kernel/declarations.cmx \
     kernel/environ.cmx kernel/esubst.cmx pretyping/evd.cmx \
-    pretyping/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/sign.cmx \
-    kernel/term.cmx pretyping/termops.cmx kernel/univ.cmx lib/util.cmx \
+    pretyping/instantiate.cmx kernel/names.cmx lib/pp.cmx \
+    kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
+    pretyping/termops.cmx kernel/univ.cmx lib/util.cmx \
     pretyping/reductionops.cmi 
 pretyping/retyping.cmo: kernel/declarations.cmi kernel/environ.cmi \
     kernel/inductive.cmi pretyping/instantiate.cmi kernel/names.cmi \
@@ -1459,13 +1463,11 @@ toplevel/minicoq.cmx: kernel/declarations.cmx toplevel/fhimsg.cmx \
     kernel/safe_typing.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/type_errors.cmx lib/util.cmx 
 toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \
-    kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
-    library/summary.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \
-    toplevel/mltop.cmi 
+    kernel/names.cmi lib/options.cmi lib/pp.cmi library/summary.cmi \
+    lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi toplevel/mltop.cmi 
 toplevel/mltop.cmx: library/lib.cmx library/libobject.cmx library/library.cmx \
-    kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
-    library/summary.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \
-    toplevel/mltop.cmi 
+    kernel/names.cmx lib/options.cmx lib/pp.cmx library/summary.cmx \
+    lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx toplevel/mltop.cmi 
 toplevel/protectedtoplevel.cmo: toplevel/errors.cmi \
     toplevel/line_oriented_parser.cmi parsing/pcoq.cmi lib/pp.cmi \
     toplevel/vernac.cmi toplevel/vernacinterp.cmi \
@@ -1561,11 +1563,13 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx \
 toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \
     library/library.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \
     parsing/pcoq.cmi lib/pp.cmi library/states.cmi lib/system.cmi \
-    lib/util.cmi toplevel/vernacinterp.cmi toplevel/vernac.cmi 
+    pretyping/termops.cmi lib/util.cmi toplevel/vernacinterp.cmi \
+    toplevel/vernac.cmi 
 toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
     library/library.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \
     parsing/pcoq.cmx lib/pp.cmx library/states.cmx lib/system.cmx \
-    lib/util.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi 
+    pretyping/termops.cmx lib/util.cmx toplevel/vernacinterp.cmx \
+    toplevel/vernac.cmi 
 contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
     contrib/correctness/past.cmi contrib/correctness/penv.cmi \
     contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
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
diff --git a/library/declare.ml b/library/declare.ml
index 9fa7b1477..816a45615 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -377,7 +377,7 @@ let last_section_hyps dir =
         if dir=p then id::sec_ids else sec_ids
       with Not_found -> sec_ids)
     (Environ.named_context (Global.env()))
-    []
+    ~init:[]
 
 let constr_of_reference = function
   | VarRef id -> mkVar id
diff --git a/library/impargs.mli b/library/impargs.mli
index 46d03d996..470f3d0c3 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -12,7 +12,6 @@
 open Names
 open Term
 open Environ
-open Inductive
 open Nametab
 (*i*)
 
diff --git a/library/lib.ml b/library/lib.ml
index 17b8fa8da..b2e73d1ce 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -129,7 +129,6 @@ let start_module s =
   if !path_prefix <> default_module then
     error "some sections are already opened";
   module_name := Some s;
-  Univ.set_module s;
   let _ = add_anonymous_entry (Module s) in
   path_prefix := s
 
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index f106d16d6..c7cfc7deb 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -13,8 +13,6 @@ open Pp
 open Names
 open Sign
 open Term
-open Termops
-open Inductive
 open Environ
 open Reductionops
 open Nametab
@@ -22,7 +20,7 @@ open Nametab
 
 (* A Pretty-Printer for the Calculus of Inductive Constructions. *)
 
-val assumptions_for_print : name list -> names_context
+val assumptions_for_print : name list -> Termops.names_context
 
 val print_closed_sections : bool ref
 val print_impl_args : int list -> std_ppcmds
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index ea3a4fdb8..b08286ef3 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -97,7 +97,7 @@ let new_evar =
 let make_evar_instance env =
   fold_named_context
     (fun env (id, b, _) l -> (*if b=None then*) mkVar id :: l (*else l*))
-    env []
+    env ~init:[]
 
 (* create an untyped existential variable *)
 let new_evar_in_sign env =
@@ -124,7 +124,7 @@ let new_Type () = mkType (new_univ ())
 
 let new_Type_sort () = Type (new_univ ())
 
-let judge_of_new_Type () = fst (Typeops.judge_of_type (new_univ ()))
+let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
 (*
 let new_Type () = mkType dummy_univ
 
@@ -304,7 +304,7 @@ let make_evar_instance_with_rel env =
   let vars = 
     fold_named_context
       (fun env (id,b,_) l -> (* if b=None then *) mkVar id :: l (*else l*))
-      env [] in
+      env ~init:[] in
   snd (fold_rel_context
     (fun env (_,b,_) (i,l) -> (i-1, (*if b=None then *) mkRel i :: l (*else l*)))
     env (n,vars))
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 066df1209..c8cbf31a6 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -18,126 +18,36 @@ open Declarations
 open Environ
 open Reductionops
 
-(*
-type inductive_instance = {
-  mis_sp : section_path;
-  mis_mib : mutual_inductive_body;
-  mis_tyi : int;
-  mis_mip : one_inductive_body }
-
-
-let build_mis (sp,tyi) mib =
-  { mis_sp = sp; mis_mib = mib; mis_tyi = tyi;
-    mis_mip = mind_nth_type_packet mib tyi }
-
-let mis_ntypes mis = mis.mis_mib.mind_ntypes
-let mis_nparams mis = mis.mis_mip.mind_nparams
-
-let mis_index mis = mis.mis_tyi
-
-let mis_nconstr mis = Array.length (mis.mis_mip.mind_consnames)
-let mis_nrealargs mis = mis.mis_mip.mind_nrealargs
-let mis_kelim mis = mis.mis_mip.mind_kelim
-let mis_recargs mis =
-  Array.map (fun mip -> mip.mind_listrec) mis.mis_mib.mind_packets
-let mis_recarg mis = mis.mis_mip.mind_listrec
-let mis_typename mis = mis.mis_mip.mind_typename
-let mis_typepath mis =
-  make_path (dirpath mis.mis_sp) mis.mis_mip.mind_typename CCI
-let mis_consnames mis = mis.mis_mip.mind_consnames
-let mis_conspaths mis =
-  let dir = dirpath mis.mis_sp in
-  Array.map (fun id -> make_path dir id CCI) mis.mis_mip.mind_consnames
-let mis_inductive mis = (mis.mis_sp,mis.mis_tyi)
-let mis_finite mis = mis.mis_mip.mind_finite
-
-let mis_typed_nf_lc mis =
-  let sign = mis.mis_mib.mind_hyps in
-  mis.mis_mip.mind_nf_lc
-
-let mis_nf_lc mis = Array.map body_of_type (mis_typed_nf_lc mis)
-
-let mis_user_lc mis = 
-  let sign = mis.mis_mib.mind_hyps in
-  (mind_user_lc mis.mis_mip)
-
-(* gives the vector of constructors and of 
-   types of constructors of an inductive definition 
-   correctly instanciated *)
-
-let mis_type_mconstructs mispec =
-  let specif = Array.map body_of_type (mis_user_lc mispec)
-  and ntypes = mis_ntypes mispec
-  and nconstr = mis_nconstr mispec in
-  let make_Ik k = mkMutInd (mispec.mis_sp,ntypes-k-1) 
-  and make_Ck k =
-     mkMutConstruct ((mispec.mis_sp,mispec.mis_tyi),k+1) in
-  (Array.init nconstr make_Ck, 
-   Array.map (substl (list_tabulate make_Ik ntypes)) specif)
-*)
-let mis_nf_constructor_type (ind,mib,mip) j =
-  let specif = mip.mind_nf_lc
-  and ntypes = mib.mind_ntypes
-  and nconstr = Array.length mip.mind_consnames in
-  let make_Ik k = mkInd ((fst ind),ntypes-k-1) in 
-  if j > nconstr then error "Not enough constructors in the type";
-  substl (list_tabulate make_Ik ntypes) specif.(j-1)
-(*
-let mis_constructor_type i mispec = 
-  let specif = mis_user_lc mispec
-  and ntypes = mis_ntypes mispec
-  and nconstr = mis_nconstr mispec in
-  let make_Ik k = mkMutInd (mispec.mis_sp,ntypes-k-1) in 
-  if i > nconstr then error "Not enough constructors in the type";
-  substl (list_tabulate make_Ik ntypes) specif.(i-1)
-
-let mis_arity mis =
-  let hyps = mis.mis_mib.mind_hyps  in
-  mind_user_arity mis.mis_mip
-
-let mis_nf_arity mis =
-  let hyps = mis.mis_mib.mind_hyps in
-  mis.mis_mip.mind_nf_arity
-
-let mis_params_ctxt mis = mis.mis_mip.mind_params_ctxt
-(*
-  let paramsign,_ =
-    decompose_prod_n_assum mis.mis_mip.mind_nparams
-      (body_of_type (mis_nf_arity mis))
-  in paramsign
-*)
-
-let mis_sort mispec = mispec.mis_mip.mind_sort
-*)
-
 (* [inductive_family] = [inductive_instance] applied to global parameters *)
 type inductive_family = inductive * constr list
 
-type inductive_type = IndType of inductive_family * constr list
+let make_ind_family (mis, params) = (mis,params)
+let dest_ind_family (mis,params) = (mis,params)
 
 let liftn_inductive_family n d (mis,params) =
   (mis, List.map (liftn n d) params)
 let lift_inductive_family n = liftn_inductive_family n 1
 
-let liftn_inductive_type n d (IndType (indf, realargs)) =
-  IndType (liftn_inductive_family n d indf, List.map (liftn n d) realargs)
-let lift_inductive_type n = liftn_inductive_type n 1
-
 let substnl_ind_family l n (mis,params) =
   (mis, List.map (substnl l n) params)
 
-let substnl_ind_type l n (IndType (indf,realargs)) =
-  IndType (substnl_ind_family l n indf, List.map (substnl l n) realargs)
 
-let make_ind_family (mis, params) = (mis,params)
-let dest_ind_family (mis,params) = (mis,params)
+type inductive_type = IndType of inductive_family * constr list
 
 let make_ind_type (indf, realargs) = IndType (indf,realargs)
 let dest_ind_type (IndType (indf,realargs)) = (indf,realargs)
 
+let liftn_inductive_type n d (IndType (indf, realargs)) =
+  IndType (liftn_inductive_family n d indf, List.map (liftn n d) realargs)
+let lift_inductive_type n = liftn_inductive_type n 1
+
+let substnl_ind_type l n (IndType (indf,realargs)) =
+  IndType (substnl_ind_family l n indf, List.map (substnl l n) realargs)
+
 let mkAppliedInd (IndType ((ind,params), realargs)) =
   applist (mkInd ind,params@realargs)
 
+
 let mis_is_recursive_subset listind mip = 
   let rec one_is_rec rvec = 
     List.exists
@@ -152,6 +62,14 @@ let mis_is_recursive_subset listind mip =
 let mis_is_recursive (mib,mip) =
   mis_is_recursive_subset (interval 0 (mib.mind_ntypes-1)) mip
 
+let mis_nf_constructor_type (ind,mib,mip) j =
+  let specif = mip.mind_nf_lc
+  and ntypes = mib.mind_ntypes
+  and nconstr = Array.length mip.mind_consnames in
+  let make_Ik k = mkInd ((fst ind),ntypes-k-1) in 
+  if j > nconstr then error "Not enough constructors in the type";
+  substl (list_tabulate make_Ik ntypes) specif.(j-1)
+
 (* Annotation for cases *)
 let make_case_info env ind style pats_source =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
@@ -200,15 +118,7 @@ let instantiate_params t args sign =
     | [], [] -> substl s t
     | _ -> anomaly"instantiate_params: type, ctxt and args mismatch"
   in inst [] t (List.rev sign,args)
-(*
-let get_constructor_type (IndFamily (mispec,params)) j =
-  assert (j <= mis_nconstr mispec);
-  let typi = mis_constructor_type j mispec in
-  instantiate_params typi params (mis_params_ctxt mispec)
-
-let get_constructors_types (IndFamily (mispec,params) as indf) =
-  Array.init (mis_nconstr mispec) (fun j -> get_constructor_type indf (j+1))
-*)
+
 let get_constructor (ind,mib,mip,params) j =
   assert (j <= Array.length mip.mind_consnames);
   let typi = mis_nf_constructor_type (ind,mib,mip) j in
@@ -340,10 +250,8 @@ let is_dep env predty (ind,args) =
   is_dep_arity env kelim predty glob_t
 
 
-
 let set_names env n brty =
-  let (args,cl) = decompose_prod_n n brty in
-  let ctxt = List.map (fun (x,ty) -> (x,None,ty)) args in
+  let (ctxt,cl) = decompose_prod_n_assum n brty in
   it_mkProd_or_LetIn_name env cl ctxt
 
 let set_pattern_names env ind brv =
@@ -365,7 +273,7 @@ let type_case_branches_with_names env indspec pj c =
 (* Guard condition *)
 
 (* A function which checks that a term well typed verifies both
-   syntaxic conditions *)
+   syntactic conditions *)
 
 let control_only_guard env = 
   let rec control_rec c = match kind_of_term c with
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 2174bf0e9..ef72ab7a3 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -11,46 +11,38 @@
 open Names
 open Term
 open Declarations
-open Sign
 open Environ
 open Evd
 
-val mis_nf_constructor_type :
-  (section_path * 'a) * mutual_inductive_body *
-  one_inductive_body -> int -> constr
-
+(* An inductive type with its parameters *)
 type inductive_family = inductive * constr list
-and inductive_type = IndType of inductive_family * constr list
-val liftn_inductive_family :
-  int -> int -> 'a * constr list -> 'a * constr list
-val lift_inductive_family :
-  int -> 'a * constr list -> 'a * constr list
-val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
-val lift_inductive_type : int -> inductive_type -> inductive_type
-val substnl_ind_family :
-  constr list -> int -> 'a * constr list -> 'a * constr list
-val substnl_ind_type :
-  constr list -> int -> inductive_type -> inductive_type
 val make_ind_family : 'a * 'b -> 'a * 'b
 val dest_ind_family : 'a * 'b -> 'a * 'b
+val liftn_inductive_family : int -> int -> inductive_family -> inductive_family
+val lift_inductive_family  : int -> inductive_family -> inductive_family
+val substnl_ind_family :
+  constr list -> int -> inductive_family -> inductive_family
+
+(* An inductive type with its parameters and real arguments *)
+type inductive_type = IndType of inductive_family * constr list
 val make_ind_type : inductive_family * constr list -> inductive_type
 val dest_ind_type : inductive_type -> inductive_family * constr list
+val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
+val lift_inductive_type  : int -> inductive_type -> inductive_type
+val substnl_ind_type :
+  constr list -> int -> inductive_type -> inductive_type
+
 val mkAppliedInd : inductive_type -> constr
-val mis_is_recursive_subset :
-  int list -> one_inductive_body -> bool
-val mis_is_recursive :
-  mutual_inductive_body * one_inductive_body ->
-  bool
-val make_case_info :
-  env -> inductive ->
-  case_style option -> pattern_source array -> case_info
-val make_default_case_info : env -> inductive -> case_info
+val mis_is_recursive_subset : int list -> one_inductive_body -> bool
+val mis_is_recursive : mutual_inductive_body * one_inductive_body -> bool
+val mis_nf_constructor_type :
+  inductive * mutual_inductive_body * one_inductive_body -> int -> constr
 
 type constructor_summary = {
   cs_cstr : constructor;
   cs_params : constr list;
   cs_nargs : int;
-  cs_args : rel_context;
+  cs_args : Sign.rel_context;
   cs_concl_realargs : constr array;
 } 
 val lift_constructor : int -> constructor_summary -> constructor_summary
@@ -59,28 +51,24 @@ val get_constructor :
   int -> constructor_summary
 val get_constructors :
   env -> inductive * constr list -> constructor_summary array
-val get_arity :
-  env -> inductive * constr list -> arity
-val local_rels : rel_context -> constr list
+val get_arity : env -> inductive * constr list -> Sign.arity
 val build_dependent_constructor : constructor_summary -> constr
 val build_dependent_inductive   : env -> inductive * constr list -> constr
-val make_arity :
-  env -> bool -> inductive * constr list -> sorts -> types
-val build_branch_type :
-  env -> bool -> constr -> constructor_summary -> types
+val make_arity : env -> bool -> inductive * constr list -> sorts -> types
+val build_branch_type : env -> bool -> constr -> constructor_summary -> types
 
 exception Induc
 val extract_mrectype : constr -> inductive * constr list
-val find_mrectype :
-  env -> evar_map -> constr -> inductive * constr list
-val find_rectype :
-  env -> evar_map -> constr -> inductive_type
-val find_inductive :
-  env -> evar_map -> constr -> inductive * constr list
-val find_coinductive :
-  env ->
-  evar_map -> constr -> inductive * constr list
+val find_mrectype    : env -> evar_map -> constr -> inductive * constr list
+val find_rectype     : env -> evar_map -> constr -> inductive_type
+val find_inductive   : env -> evar_map -> constr -> inductive * constr list
+val find_coinductive : env -> evar_map -> constr -> inductive * constr list
+
 val type_case_branches_with_names :
   env -> inductive * constr list -> unsafe_judgment -> constr ->
     types array * types
+val make_case_info :
+  env -> inductive -> case_style option -> pattern_source array -> case_info
+val make_default_case_info : env -> inductive -> case_info
+
 val control_only_guard : env -> types -> unit
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index fd42ca0ba..034597a71 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -55,7 +55,7 @@ let env_ise sigma env =
         (na, option_app (nf_evar sigma) b, nf_evar sigma ty)
         e)
     ctxt
-    env0
+    ~init:env0
 
 (* This simplify the typing context of Cases clauses *)
 (* hope it does not disturb other typing contexts *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a601d6397..a98cc3e81 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -305,7 +305,7 @@ let rec pretype tycon env isevars lvar lmeta = function
       let env' = push_rel_assum var env in
       let j' = pretype_type empty_valcon env' isevars lvar lmeta c2 in
       let resj =
-	try fst (judge_of_product env name j j')
+	try judge_of_product env name j j'
 	with TypeError _ as e -> Stdpp.raise_with_loc loc e in
       inh_conv_coerce_to_tycon loc env isevars resj tycon
 	
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index bb6948767..da12c6449 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -90,7 +90,7 @@ let typeur sigma metamap =
     match kind_of_term t with
     | Cast (c,s) when isSort s -> destSort s
     | Sort (Prop c) -> type_0
-    | Sort (Type u) -> Type (fst (Univ.super u))
+    | Sort (Type u) -> Type (Univ.super u)
     | Prod (name,t,c2) ->
         (match (sort_of (push_rel (name,None,t) env) c2) with
 	  | Prop _ as s -> s
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index f8dd8ce15..04cbd0d19 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -23,6 +23,23 @@ let print_sort = function
 (*  | Type _ -> [< 'sTR "Type" >] *)
   | Type u -> [< 'sTR "Type("; Univ.pr_uni u; 'sTR ")" >]
 
+let current_module = ref empty_dirpath
+
+let set_module m = current_module := m
+
+let new_univ = 
+  let univ_gen = ref 0 in
+  (fun sp ->
+    incr univ_gen; 
+    Univ.make_univ (!current_module,!univ_gen))
+
+let new_sort_in_family = function 
+  | InProp -> mk_Prop
+  | InSet -> mk_Set
+  | InType -> Type (new_univ ())
+
+
+
 (* prod_it b [xn:Tn;..;x1:T1] = (x1:T1)..(xn:Tn)b *)
 let prod_it = List.fold_left (fun c (n,t)  -> mkProd (n, t, c))
 
@@ -580,9 +597,9 @@ let empty_names_context = []
 let ids_of_rel_context sign =
   Sign.fold_rel_context
     (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l)
-    sign []
+    sign ~init:[]
 let ids_of_named_context sign =
-  Sign.fold_named_context (fun (id,_,_) idl -> id::idl) sign []
+  Sign.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[]
 
 let ids_of_context env = 
   (ids_of_rel_context (rel_context env))
@@ -673,7 +690,7 @@ let process_rel_context f env =
   let sign = named_context env in
   let rels = rel_context env in
   let env0 = reset_with_named_context sign env in
-  Sign.fold_rel_context f rels env0
+  Sign.fold_rel_context f rels ~init:env0
 
 let assums_of_rel_context sign =
   Sign.fold_rel_context
@@ -681,7 +698,7 @@ let assums_of_rel_context sign =
       match c with
           Some _ -> l
         | None -> (na,body_of_type t)::l)
-    sign []
+    sign ~init:[]
 
 let lift_rel_context n sign =
   let rec liftrec k = function
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 30a7fa8ca..5e32cef35 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -15,6 +15,12 @@ open Term
 open Sign
 open Environ
 
+(* Universes *)
+val set_module : Names.dir_path -> unit
+val new_univ : unit -> Univ.universe
+val new_sort_in_family : sorts_family -> sorts
+
+(* iterators on terms *)
 val print_sort : sorts -> std_ppcmds
 val prod_it : init:types -> (name * types) list -> types
 val lam_it : init:constr -> (name * types) list -> constr
@@ -138,6 +144,6 @@ val assums_of_rel_context : rel_context -> (name * constr) list
 val lift_rel_context : int -> rel_context -> rel_context
 val fold_named_context_both_sides :
   ('a -> named_declaration -> named_context -> 'a) ->
-    named_context -> 'a -> 'a
+    named_context -> init:'a -> 'a
 val mem_named_context : identifier -> named_context -> bool
 val make_all_name_different : env -> env
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index b36c03204..5b759e74c 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -86,7 +86,7 @@ let rec execute mf env sigma cstr =
 	judge_of_prop_contents c
 
     | Sort (Type u) ->
-	let (j,_) = judge_of_type u in j
+	judge_of_type u
 	  
     | App (f,args) ->
 	let j = execute mf env sigma f in
@@ -107,8 +107,7 @@ let rec execute mf env sigma cstr =
 	let env1 = push_rel (name,None,varj.utj_val) env in
         let j' = execute mf env1 sigma c2 in
         let varj' = type_judgment env sigma j' in
-	let (j,_) = judge_of_product env1 name varj varj' in
-	j
+	judge_of_product env1 name varj varj'
 
      | LetIn (name,c1,c2,c3) ->
         let j1 = execute mf env sigma c1 in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index cdb45cced..6043857fa 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -243,7 +243,7 @@ let apply_to_hyp sign id f =
 	   found := true; f sign d tail
 	 end else 
 	   add_named_decl d sign)
-      sign empty_named_context
+      sign ~init:empty_named_context
   in
   if (not !check) || !found then sign' else error "No such assumption"
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 921238d45..e7b2c78f7 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -57,7 +57,7 @@ let norm_goal sigma gl =
     Sign.fold_named_context 
       (fun (d,b,ty) sign ->
         add_named_decl (d, option_app red_fun b, red_fun ty) sign)
-      empty_named_context gl.evar_hyps;
+      gl.evar_hyps ~init:empty_named_context;
     evar_body = gl.evar_body}
 
 
@@ -799,7 +799,7 @@ let thin_sign osign sign =
 	 if Sign.lookup_named id osign = (id,c,ty) then sign
 	 else raise Different
        with Not_found | Different -> add_named_decl d sign)
-    sign empty_named_context
+    sign ~init:empty_named_context
 
 let rec print_proof sigma osign pf =
   let {evar_hyps=hyps; evar_concl=cl; 
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 2fa36bf20..a3bca6d23 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -221,7 +221,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
       (fun env (id,_,_ as d) sign ->
          if mem_named_context id global_named_context then sign
 	 else add_named_decl d sign)
-      invEnv empty_named_context 
+      invEnv ~init:empty_named_context 
   in
   let (_,ownSign,mvb) =
     List.fold_left
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d20712b5d..804555583 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -666,10 +666,14 @@ let generalize_dep c gl =
       or dependent_in_decl c d then 
       d::toquant
     else 
-      toquant
-  in
-  let to_quantify = List.fold_left seek [] sign in
-  let qhyps = List.map (fun (id,_,_) -> id) to_quantify in
+      toquant in
+  let toq_rev = Sign.fold_named_context_reverse seek [] sign in
+  let qhyps = List.map (fun (id,_,_) -> id) toq_rev in
+  let to_quantify =
+    List.fold_left
+      (fun sign d -> add_named_decl d sign)
+      empty_named_context
+      toq_rev in
   let tothin = List.filter (fun id -> not (List.mem id init_ids)) qhyps in
   let tothin' =
     match kind_of_term c with
@@ -677,9 +681,9 @@ let generalize_dep c gl =
 	  -> id::tothin
       | _ -> tothin
   in
-  let cl' = List.fold_right mkNamedProd_or_LetIn to_quantify (pf_concl gl) in
+  let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in
   let cl'' = generalize_goal gl c cl' in
-  let args = Array.to_list (instance_from_named_context to_quantify) in
+  let args = List.map mkVar qhyps in
   tclTHEN
     (apply_type cl'' (c::args))
     (thin (List.rev tothin'))
@@ -766,9 +770,14 @@ let letin_tac with_eq name c occs gl =
       if not (mem_named_context x (named_context env)) then x else
 	error ("The variable "^(string_of_id x)^" is already declared") in
   let (depdecls,marks,ccl)= letin_abstract id c occs gl in 
+  let ctxt =
+    List.fold_left
+      (fun sign d -> add_named_decl d sign)
+      empty_named_context
+      depdecls in
   let t = pf_type_of gl c in
   let tmpcl = List.fold_right mkNamedProd_or_LetIn depdecls ccl in
-  let args = Array.to_list (instance_from_named_context depdecls) in
+  let args = List.map (fun (id,_,_) -> mkVar id) depdecls in
   let newcl = mkNamedLetIn id c t tmpcl in
 (*
     if with_eq then
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 5e0132468..a6fbb7283 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -128,7 +128,7 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
         Sign.add_named_decl
           (x, option_app (expmod_constr modlist) b,expmod_constr modlist t)
           sgn)
-      mib.mind_hyps empty_named_context in
+      mib.mind_hyps ~init:empty_named_context in
   let (inds',abs_vars) = abstract_inductive ids_to_discard hyps' inds in
   let lmodif_one_mind i = 
     let nbc = Array.length mib.mind_packets.(i).mind_consnames in 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index da11dddaa..f683e7b44 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -34,6 +34,10 @@ let explain_unbound_rel ctx n =
   [< 'sTR"Unbound reference: "; pe;
      'sTR"The reference "; 'iNT n; 'sTR" is free" >]
 
+let explain_unbound_var ctx v =
+  let var = pr_id v in
+  [< 'sTR"No such section variable or assumption : "; var >]
+
 let explain_not_type ctx j =
   let ctx = make_all_name_different ctx in
   let pe = pr_ne_context_of [< 'sTR"In environment" >] ctx in
@@ -288,6 +292,8 @@ let explain_wrong_case_info ctx ind ci =
 let explain_type_error ctx = function
   | UnboundRel n -> 
       explain_unbound_rel ctx n
+  | UnboundVar v -> 
+      explain_unbound_var ctx v
   | NotAType j -> 
       explain_not_type ctx j
   | BadAssumption c -> 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7090384bc..89a3e10b9 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -160,6 +160,7 @@ let compile verbosely f =
     let _,longf = find_file_in_path (Library.get_load_path ()) (f^".v") in
     let ldir0 = Library.find_logical_path (Filename.dirname longf) in
     let ldir = Nameops.extend_dirpath ldir0 m in
+    Termops.set_module ldir; (* Just for universe naming *)
     Lib.start_module ldir;
     let _ = load_vernac verbosely longf in
     let mid = Lib.end_module m in