retablissement make doc et make minicoq

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

17 files changed, 109 insertions, 97 deletions

diff --git a/.depend b/.depend
index 3e97c1667d..ba4d941ee6 100644
--- a/.depend
+++ b/.depend
@@ -32,6 +32,8 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.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 
+lib/system.cmi: lib/pp.cmi 
+lib/util.cmi: lib/pp.cmi 
 library/declare.cmi: kernel/declarations.cmi kernel/environ.cmi \
     kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
 library/global.cmi: kernel/declarations.cmi kernel/environ.cmi \
@@ -47,8 +49,6 @@ library/library.cmi: lib/pp.cmi
 library/nametab.cmi: kernel/names.cmi 
 library/redinfo.cmi: kernel/names.cmi kernel/term.cmi 
 library/summary.cmi: kernel/names.cmi 
-lib/system.cmi: lib/pp.cmi 
-lib/util.cmi: lib/pp.cmi 
 parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     parsing/pcoq.cmi lib/pp.cmi 
 parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
@@ -187,11 +187,11 @@ toplevel/record.cmi: parsing/coqast.cmi kernel/names.cmi kernel/term.cmi
 toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
     kernel/term.cmi 
 toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi 
+toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi 
 toplevel/vernacentries.cmi: kernel/names.cmi kernel/term.cmi \
     toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     proofs/proof_type.cmi 
-toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi 
 config/coq_config.cmo: config/coq_config.cmi 
 config/coq_config.cmx: config/coq_config.cmi 
 dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi 
@@ -318,22 +318,30 @@ lib/dyn.cmo: lib/util.cmi lib/dyn.cmi
 lib/dyn.cmx: lib/util.cmx lib/dyn.cmi 
 lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi 
 lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi 
-lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi 
-lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi 
 lib/gmap.cmo: lib/gmap.cmi 
 lib/gmap.cmx: lib/gmap.cmi 
+lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi 
+lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi 
 lib/gset.cmo: lib/gset.cmi 
 lib/gset.cmx: lib/gset.cmi 
 lib/hashcons.cmo: lib/hashcons.cmi 
 lib/hashcons.cmx: lib/hashcons.cmi 
 lib/options.cmo: lib/util.cmi lib/options.cmi 
 lib/options.cmx: lib/util.cmx lib/options.cmi 
-lib/pp_control.cmo: lib/pp_control.cmi 
-lib/pp_control.cmx: lib/pp_control.cmi 
 lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
 lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
+lib/pp_control.cmo: lib/pp_control.cmi 
+lib/pp_control.cmx: lib/pp_control.cmi 
 lib/profile.cmo: lib/system.cmi lib/profile.cmi 
 lib/profile.cmx: lib/system.cmx lib/profile.cmi 
+lib/stamps.cmo: lib/stamps.cmi 
+lib/stamps.cmx: lib/stamps.cmi 
+lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi 
+lib/system.cmx: lib/pp.cmx lib/util.cmx lib/system.cmi 
+lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
+lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
+lib/util.cmo: lib/pp.cmi lib/util.cmi 
+lib/util.cmx: lib/pp.cmx lib/util.cmi 
 library/declare.cmo: kernel/declarations.cmi kernel/environ.cmi \
     kernel/evd.cmi kernel/generic.cmi library/global.cmi library/impargs.cmi \
     library/indrec.cmi kernel/inductive.cmi library/lib.cmi \
@@ -410,14 +418,6 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
     library/summary.cmi 
 library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
     library/summary.cmi 
-lib/stamps.cmo: lib/stamps.cmi 
-lib/stamps.cmx: lib/stamps.cmi 
-lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi 
-lib/system.cmx: lib/pp.cmx lib/util.cmx lib/system.cmi 
-lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
-lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
-lib/util.cmo: lib/pp.cmi lib/util.cmi 
-lib/util.cmx: lib/pp.cmx lib/util.cmi 
 parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \
     kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi 
 parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \
@@ -994,8 +994,12 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \
     lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx \
     pretyping/retyping.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \
     lib/util.cmx tactics/wcclausenv.cmi 
-tools/coqdep.cmo: config/coq_config.cmi 
-tools/coqdep.cmx: config/coq_config.cmx 
+tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
+tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
+tools/coqdep_lexer.cmo: config/coq_config.cmi 
+tools/coqdep_lexer.cmx: config/coq_config.cmx 
+tools/gallina.cmo: tools/gallina_lexer.cmo 
+tools/gallina.cmx: tools/gallina_lexer.cmx 
 toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
     kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
     kernel/evd.cmi kernel/generic.cmi library/global.cmi library/indrec.cmi \
@@ -1114,6 +1118,14 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmi \
     toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi 
 toplevel/usage.cmo: toplevel/usage.cmi 
 toplevel/usage.cmx: toplevel/usage.cmi 
+toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \
+    lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
+    library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \
+    toplevel/vernac.cmi 
+toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
+    lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \
+    library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \
+    toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
     pretyping/class.cmi toplevel/command.cmi parsing/coqast.cmi \
     library/declare.cmi toplevel/discharge.cmi kernel/environ.cmi \
@@ -1150,14 +1162,6 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx toplevel/command.cmx \
     parsing/coqast.cmx lib/dyn.cmx toplevel/himsg.cmx kernel/names.cmx \
     lib/options.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
     lib/util.cmx toplevel/vernacinterp.cmi 
-toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \
-    lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
-    library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \
-    toplevel/vernac.cmi 
-toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
-    lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \
-    library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \
-    toplevel/vernac.cmi 
 contrib/omega/coq_omega.cmo: parsing/ast.cmi proofs/clenv.cmi \
     library/declare.cmi kernel/environ.cmi tactics/equality.cmi \
     kernel/generic.cmi library/global.cmi kernel/inductive.cmi \
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 616a111620..981be607fc 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -49,21 +49,21 @@ val names_of_rel_context : env -> names_context
 (*s Returns also the substitution to be applied to rel's *)
 val push_rels_to_vars : env -> constr list * env
 
-(* Gives identifiers in var_context and rel_context *)
+(* Gives identifiers in [var_context] and [rel_context] *)
 val ids_of_context : env -> identifier list
 val map_context : (constr -> constr) -> env -> env
 
-(*s Recurrence on var_context *)
+(*s Recurrence on [var_context] *)
 val fold_var_context : (env -> var_declaration -> 'a -> 'a) -> env -> 'a -> 'a
 val process_var_context : (env -> var_declaration -> env) -> env -> env
 
 (* [process_var_context_both_sides f env] iters [f] on the var
-   declarations of env taking as argument both the initial segment, the
+   declarations of [env] taking as argument both the initial segment, the
    middle value and the tail segment *)
 val process_var_context_both_sides :
   (env -> var_declaration -> var_context -> env) -> env -> env 
 
-(*s Recurrence on rel_context *)
+(*s Recurrence on [rel_context] *)
 val fold_rel_context : (env -> rel_declaration -> 'a -> 'a) -> env -> 'a -> 'a
 val process_rel_context : (env -> rel_declaration -> env) -> env -> env
 
@@ -81,13 +81,13 @@ val new_meta : unit -> int
 
 (*s Looks up in environment *)
 
-(* Looks up in the context of local vars referred by names (var_context) *)
+(* Looks up in the context of local vars referred by names ([var_context]) *)
 (* raises [Not_found] if the identifier is not found *)
 val lookup_var_type : identifier -> env -> typed_type
 val lookup_var_value : identifier -> env -> constr option
 val lookup_var : identifier -> env -> constr option * typed_type
 
-(* Looks up in the context of local vars referred by indice (rel_context) *)
+(* Looks up in the context of local vars referred by indice ([rel_context]) *)
 (* raises [Not_found] if the index points out of the context *)
 val lookup_rel_type : int -> env -> name * typed_type
 val lookup_rel_value : int -> env -> constr option
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 6d8c80bd0d..c2fb4a3c09 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -28,10 +28,10 @@ val var_context : safe_environment -> var_context
 
 val push_var_decl : identifier * constr -> safe_environment -> safe_environment
 val push_var_def : identifier * constr -> safe_environment -> safe_environment
-(*
+(*i
 val push_rel_decl : name * constr -> safe_environment -> safe_environment
 val push_rel_def : name * constr -> safe_environment -> safe_environment
-*)
+i*)
 
 val add_constant : 
   section_path -> constant_entry -> safe_environment -> safe_environment
@@ -48,9 +48,9 @@ val add_constraints : constraints -> safe_environment -> safe_environment
 val pop_vars : identifier list -> safe_environment -> safe_environment
 
 val lookup_var : identifier -> safe_environment -> constr option * typed_type
-(*
+(*i
 val lookup_rel : int -> safe_environment -> name * typed_type
-*)
+i*)
 val lookup_constant : section_path -> safe_environment -> constant_body
 val lookup_mind : section_path -> safe_environment -> mutual_inductive_body
 val lookup_mind_specif : inductive -> safe_environment -> inductive_instance
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 3add55894c..17d9267d98 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -7,13 +7,15 @@ open Generic
 open Term
 (*i*)
 
-(*s Signatures of _ordered_ named variables, intended to be accessed by name *)
+(*s Signatures of ordered named variables, intended to be accessed by name *)
 
 type var_context = var_declaration list
 
-val add_var : identifier * constr option * typed_type -> var_context -> var_context
+val add_var : 
+  identifier * constr option * typed_type -> var_context -> var_context
 val add_var_decl : identifier * typed_type -> var_context -> var_context
-val add_var_def : identifier * constr * typed_type -> var_context ->var_context
+val add_var_def : 
+  identifier * constr * typed_type -> var_context -> var_context
 val lookup_id : identifier -> var_context -> constr option * typed_type
 val lookup_id_type : identifier -> var_context -> typed_type
 val lookup_id_value : identifier -> var_context -> constr option 
diff --git a/kernel/term.mli b/kernel/term.mli
index 9019fa091f..cd86af6756 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -100,7 +100,7 @@ type 'ctxt reference =
 
 (* Concrete type for making pattern-matching. *)
 
-(* [constr array] is an instance matching definitional var_context in
+(* [constr array] is an instance matching definitional [var_context] in
    the same order (i.e. last argument first) *)
 type existential = int * constr array
 type constant = section_path * constr array
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index a07206fb0f..a2fedf7f16 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -84,7 +84,7 @@ open Inductive
 val find_case_dep_nparams :
   env -> 'a evar_map -> constr * constr -> inductive_family -> constr -> bool
 
-(*
+(*i
 val hyps_inclusion : env -> 'a evar_map -> var_context -> var_context -> bool
-*)
+i*)
 
diff --git a/library/global.mli b/library/global.mli
index c2e8ac386c..b51ce3c774 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -25,11 +25,11 @@ val var_context : unit -> var_context
 
 val push_var_decl : identifier * constr -> unit
 val push_var_def : identifier * constr -> unit
-(*
+(*i
 val push_var : identifier * constr option * constr -> unit
 val push_rel_decl : name * constr -> unit
 val push_rel_def : name * constr -> unit
-*)
+i*)
 val add_constant : section_path -> constant_entry -> unit
 val add_parameter : section_path -> constr -> unit
 val add_mind : section_path -> mutual_inductive_entry -> unit
@@ -38,7 +38,7 @@ val add_constraints : constraints -> unit
 val pop_vars : identifier list -> unit
 
 val lookup_var : identifier -> constr option * typed_type
-(*val lookup_rel : int -> name * typed_type*)
+(*i val lookup_rel : int -> name * typed_type i*)
 val lookup_constant : section_path -> constant_body
 val lookup_mind : section_path -> mutual_inductive_body
 val lookup_mind_specif : inductive -> inductive_instance
diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
index c14c5d0344..21163804ec 100644
--- a/parsing/g_minicoq.ml4
+++ b/parsing/g_minicoq.ml4
@@ -7,7 +7,7 @@ open Names
 open Univ
 open Generic
 open Term
-open Sign
+open Environ
 
 let lexer = {
   Token.func = Lexer.func;
@@ -176,5 +176,5 @@ let rec pp bv = function
   | Rel n -> print_rel bv n
   | _ -> [< 'sTR"<???>" >]
 
-let pr_term _ ctx = pp (it_dbenv (fun l n _ -> n::l) [] ctx)
+let pr_term _ ctx = pp (fold_rel_context (fun _ (n,_,_) l -> n::l) ctx [])
 
diff --git a/parsing/g_minicoq.mli b/parsing/g_minicoq.mli
index de3a022862..db5c0d07f5 100644
--- a/parsing/g_minicoq.mli
+++ b/parsing/g_minicoq.mli
@@ -3,7 +3,7 @@
 open Pp
 open Names
 open Term
-open Sign
+open Environ
 (*i*)
 
 val term : constr Grammar.Entry.e
@@ -19,4 +19,4 @@ type command =
 
 val command : command Grammar.Entry.e
 
-val pr_term : path_kind -> context -> constr -> std_ppcmds
+val pr_term : path_kind -> env -> constr -> std_ppcmds
diff --git a/proofs/logic.mli b/proofs/logic.mli
index dd27797254..9247d4ff6e 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -10,20 +10,19 @@ open Environ
 open Proof_type
 (*i*)
 
-(* This suppresses check done in prim_refiner for the tactic given in
+(* This suppresses check done in [prim_refiner] for the tactic given in
    argument; works by side-effect *)
 
 val without_check : tactic -> tactic
 
-(* without_check respectively means:\\
-\\
-  Intro: no check that the name does not exist\\
-  Intro_after: no check that the name does not exist and that variables in
+(* [without_check] respectively means:\\
+  [Intro]: no check that the name does not exist\\
+  [Intro_after]: no check that the name does not exist and that variables in
      its type does not escape their scope\\
-  Intro_replacing: no check that the name does not exist and that variables in
-     its type does not escape their scope\\
-
-  Convert_hyp: no check that the name exist and that its type is convertible\\
+  [Intro_replacing]: no check that the name does not exist and that 
+     variables in its type does not escape their scope\\
+  [Convert_hyp]: 
+  no check that the name exist and that its type is convertible\\
 *)
 
 (* The primitive refiner. *)
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 39351dc1e5..50b454df8f 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -37,7 +37,7 @@ val val_interp : interp_sign -> Coqast.t -> value
 val interp_tacarg : interp_sign -> Coqast.t -> tactic_arg
 
 val interp               : Coqast.t -> tactic
-(*val vernac_interp        : Coqast.t -> tactic*)
+(*i val vernac_interp        : Coqast.t -> tactic i*)
 val vernac_interp_atomic : identifier -> tactic_arg list -> tactic
 
 val is_just_undef_macro  : Coqast.t -> string option
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 6ae4f9ae26..bf2b0a3bab 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -34,7 +34,7 @@ val apply_sig_tac :
 val pf_concl              : goal sigma -> constr
 val pf_env                : goal sigma -> env
 val pf_hyps               : goal sigma -> var_context
-(*val pf_untyped_hyps       : goal sigma -> (identifier * constr) list*)
+(*i val pf_untyped_hyps       : goal sigma -> (identifier * constr) list i*)
 val pf_hyps_types         : goal sigma -> (identifier * constr) list
 val pf_nth_hyp_id         : goal sigma -> int -> identifier
 val pf_last_hyp           : goal sigma -> var_declaration
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
index 6efd48d555..b364706ca1 100644
--- a/tactics/tacentries.mli
+++ b/tactics/tacentries.mli
@@ -15,7 +15,7 @@ val v_symmetry      : tactic_arg list -> tactic
 val v_transitivity  : tactic_arg list -> tactic
 val v_intro         : tactic_arg list -> tactic
 val v_introsUntil   : tactic_arg list -> tactic
-(*val v_tclIDTAC      : tactic_arg list -> tactic*)
+(*i val v_tclIDTAC      : tactic_arg list -> tactic i*)
 val v_assumption    : tactic_arg list -> tactic
 val v_exact         : tactic_arg list -> tactic
 val v_reduce        : tactic_arg list -> tactic
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 0cdedd8c68..4b89938276 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -37,8 +37,10 @@ val tclLAST_HYP      : (constr -> tactic) -> tactic
 val tclTRY_sign      : (constr -> tactic) -> var_context -> tactic
 val tclTRY_HYPS      : (constr -> tactic) -> tactic
 
-(*val dyn_tclIDTAC     : tactic_arg list -> tactic
-val dyn_tclFAIL      : tactic_arg list -> tactic*)
+(*i
+val dyn_tclIDTAC     : tactic_arg list -> tactic
+val dyn_tclFAIL      : tactic_arg list -> tactic
+i*)
 
 (*s Clause tacticals. *)
 
@@ -103,7 +105,7 @@ type branch_assumptions = {
   indargs   : identifier list} (* the inductive arguments *)
 
 val sort_of_goal      : goal sigma -> sorts
-(*val suff              : goal sigma -> constr -> string*)
+(*i val suff              : goal sigma -> constr -> string i*)
 
 val general_elim_then_using :
   constr ->  (inductive -> int -> bool list) -> 
diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
index dcc0a86976..9d0e9558a6 100644
--- a/toplevel/fhimsg.ml
+++ b/toplevel/fhimsg.ml
@@ -13,13 +13,13 @@ open Reduction
 open G_minicoq
 
 module type Printer = sig
-  val pr_term : path_kind -> context -> constr -> std_ppcmds
+  val pr_term : path_kind -> env -> constr -> std_ppcmds
 end
 
 module Make = functor (P : Printer) -> struct
 
-  let print_decl k sign (s,typ) =
-    let ptyp = P.pr_term k (gLOB sign) (body_of_type typ) in 
+  let print_decl k env (s,typ) =
+    let ptyp = P.pr_term k env (body_of_type typ) in 
     [< 'sPC; print_id s; 'sTR" : "; ptyp >]
   
   let print_binding k env = function
@@ -28,34 +28,38 @@ module Make = functor (P : Printer) -> struct
     | Name id,ty -> 
 	[< 'sPC; print_id id ; 'sTR" : "; P.pr_term k env (body_of_type ty) >]
 
+(****
   let sign_it_with f sign e =
-    snd (sign_it 
-	   (fun id t (sign,e) -> (add_sign (id,t) sign, f id t sign e))
-           sign (nil_sign,e))
+    snd (fold_var_context
+	   (fun (id,v,t) (sign,e) -> (add_var (id,v,t) sign, f id t sign e))
+           sign (empty_var_context,e))
 
   let dbenv_it_with f env e =
     snd (dbenv_it 
 	   (fun na t (env,e) -> (add_rel (na,t) env, f na t env e))
            env (gLOB(get_globals env),e))
+****)
       
   let pr_env k env =
     let sign_env =
-      sign_it_with
-	(fun id t sign pps ->
-           let pidt =  print_decl k sign (id,t) in [<  pps ; 'fNL ; pidt >])
-	(get_globals env) [< >] 
+      fold_var_context
+	(fun env (id,_,t) pps ->
+           let pidt =  print_decl k env (id,t) in [<  pps ; 'fNL ; pidt >])
+	env [< >] 
     in
     let db_env =
-      dbenv_it_with 
-	(fun na t env pps ->
+      fold_rel_context
+	(fun env (na,_,t) pps ->
            let pnat = print_binding k env (na,t) in [<  pps ; 'fNL ; pnat >])
 	env [< >]
     in 
     [< sign_env; db_env >]
     
-  let pr_ne_ctx header k = function
-    | ENVIRON (s1,s2) when s1=nil_sign & s2=nil_dbsign -> [< >]
-    | env -> [< header; pr_env k env >]
+  let pr_ne_ctx header k env =
+    if rel_context env = [] && var_context env = [] then
+      [< >]
+    else
+      [< header; pr_env k env >]
 
 
 let explain_unbound_rel k ctx n =
@@ -129,7 +133,7 @@ let explain_ill_formed_branch k ctx c i actty expty =
 let explain_generalization k ctx (name,var) c =
   let pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in
   let pv = P.pr_term k ctx (body_of_type var) in
-  let pc = P.pr_term k (add_rel (name,var) ctx) c in
+  let pc = P.pr_term k (push_rel (name,None,var) ctx) c in
   [< 'sTR"Illegal generalization: "; pe; 'fNL;
      'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC;
      'sTR"over"; 'bRK(1,1); pc; 'sPC;
diff --git a/toplevel/fhimsg.mli b/toplevel/fhimsg.mli
index eb8d615538..ad0e7e6646 100644
--- a/toplevel/fhimsg.mli
+++ b/toplevel/fhimsg.mli
@@ -15,53 +15,53 @@ open Type_errors
    context. *)
 
 module type Printer = sig
-  val pr_term : path_kind -> context -> constr -> std_ppcmds
+  val pr_term : path_kind -> env -> constr -> std_ppcmds
 end
 
 (*s The result is a module which provides a function [explain_type_error]
-  to explain a type error for a given kind in a given context, which are 
+  to explain a type error for a given kind in a given env, which are 
   usually the three arguments carried by the exception [TypeError] 
   (see \refsec{typeerrors}). *)
 
 module Make (P : Printer) : sig
 
-val explain_type_error : path_kind -> context -> type_error -> std_ppcmds
+val explain_type_error : path_kind -> env -> type_error -> std_ppcmds
 
-val pr_ne_ctx : std_ppcmds -> path_kind -> context -> std_ppcmds
+val pr_ne_ctx : std_ppcmds -> path_kind -> env -> std_ppcmds
 
-val explain_unbound_rel : path_kind -> context -> int -> std_ppcmds
+val explain_unbound_rel : path_kind -> env -> int -> std_ppcmds
 
-val explain_not_type : path_kind -> context -> constr -> std_ppcmds
+val explain_not_type : path_kind -> env -> constr -> std_ppcmds
 
-val explain_bad_assumption : path_kind -> context -> constr -> std_ppcmds
+val explain_bad_assumption : path_kind -> env -> constr -> std_ppcmds
  
 val explain_reference_variables : identifier -> std_ppcmds
 
 val explain_elim_arity : 
-  path_kind -> context -> constr -> constr list -> constr 
+  path_kind -> env -> constr -> constr list -> constr 
     -> constr -> constr -> (constr * constr * string) option -> std_ppcmds
 
 val explain_case_not_inductive : 
-  path_kind -> context -> constr -> constr -> std_ppcmds
+  path_kind -> env -> constr -> constr -> std_ppcmds
 
 val explain_number_branches : 
-  path_kind -> context -> constr -> constr -> int -> std_ppcmds
+  path_kind -> env -> constr -> constr -> int -> std_ppcmds
 
 val explain_ill_formed_branch :
-  path_kind -> context -> constr -> int -> constr -> constr -> std_ppcmds
+  path_kind -> env -> constr -> int -> constr -> constr -> std_ppcmds
 
 val explain_generalization :
-  path_kind -> context -> name * typed_type -> constr -> std_ppcmds
+  path_kind -> env -> name * typed_type -> constr -> std_ppcmds
 
 val explain_actual_type :
-  path_kind -> context -> constr -> constr -> constr -> std_ppcmds
+  path_kind -> env -> constr -> constr -> constr -> std_ppcmds
 
 val explain_ill_formed_rec_body :
-  path_kind -> context -> std_ppcmds -> 
+  path_kind -> env -> std_ppcmds -> 
     name list -> int -> constr array -> std_ppcmds
 
 val explain_ill_typed_rec_body  :
-  path_kind -> context -> int -> name list -> unsafe_judgment array 
+  path_kind -> env -> int -> name list -> unsafe_judgment array 
     -> typed_type array -> std_ppcmds
 
 end
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 59253eb072..5df900c264 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -23,7 +23,8 @@ let lookup_var id =
   in
   look 1
 
-let args sign = Array.of_list (List.map (fun id -> VAR id) (ids_of_sign sign))
+let args sign = 
+  Array.of_list (List.map (fun id -> VAR id) (ids_of_var_context sign))
 
 let rec globalize bv = function
   | VAR id -> lookup_var id bv
@@ -45,7 +46,7 @@ let check c =
   let c = globalize [] c in
   let (j,u) = safe_machine !env c in
   let ty = j_type j in
-  let pty = pr_term CCI (context !env) ty in
+  let pty = pr_term CCI (env_of_safe_env !env) ty in
   mSGNL (hOV 0 [< 'sTR"  :"; 'sPC; hOV 0 pty; 'fNL >])
 
 let definition id ty c =
@@ -65,7 +66,7 @@ let parameter id t =
 
 let variable id t =
   let t = globalize [] t in
-  env := push_var (id,t) !env;
+  env := push_var_decl (id,t) !env;
   mSGNL (hOV 0 [< 'sTR"variable"; 'sPC; print_id id; 
 		  'sPC; 'sTR"is declared"; 'fNL >])