Passage à des contextes de vars et de rels pouvant contenir des déclarations

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

7 files changed, 248 insertions, 254 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 841a571e9d..002925e167 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -167,24 +167,32 @@ let ref_from_constr = function
   | VAR id -> RVar id  (* utilisé pour coe_value (tmp) *)
   | _ -> anomaly "Not a reference"
 
-let dbize_ref k sigma env loc s =
+(* [vars1] is a set of name to avoid (used for the tactic language);
+   [vars2] is the set of global variables, env is the set of variables
+   abstracted until this point *)
+let dbize_ref k sigma env loc s (vars1,vars2)=
   let id = ident_of_nvar loc s in
+  if Idset.mem id env then
+    RRef (loc,RVar id),[]
+  else
+  if List.mem s vars1 then
+    RRef(loc,RVar id),[]
+  else
+  try
+    let _ = lookup_id id vars2 in
+    RRef (loc,RVar id), (try implicits_of_var id with _ -> [])
+  with Not_found ->
   try 
-    match lookup_id id env with
-      | RELNAME(n,_) -> RRef (loc,RVar id),[]
-      | _ -> RRef(loc,RVar id), (try implicits_of_var id with _ -> [])
+    let c,il = match k with
+      | CCI -> Declare.global_reference_imps CCI id
+      | FW  -> Declare.global_reference_imps FW id
+      | OBJ -> anomaly "search_ref_cci_fw" in
+    RRef (loc,ref_from_constr c), il
   with Not_found ->
-    try 
-      let c,il = match k with
-	| CCI -> Declare.global_reference_imps CCI id
-	| FW  -> Declare.global_reference_imps FW id
-	| OBJ -> anomaly "search_ref_cci_fw" in
-      RRef (loc,ref_from_constr c), il
-    with Not_found ->
-      try 
-	(Syntax_def.search_syntactic_definition id, [])
-      with Not_found -> 
-	error_var_not_found_loc loc CCI id
+  try 
+    (Syntax_def.search_syntactic_definition id, [])
+  with Not_found -> 
+    error_var_not_found_loc loc CCI id
 	  
 let mkLambdaC (x,a,b) = ope("LAMBDA",[a;slam(Some (string_of_id x),b)])
 let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
@@ -268,22 +276,18 @@ let check_capture s ty = function
 
 let dbize k sigma env allow_soapp lvar =
   let rec dbrec env = function
-    | Nvar(loc,s) ->
-      if List.mem s lvar then
-        RRef(loc,RVar (id_of_string s))
-      else
-        fst (dbize_ref k sigma env loc s)
+    | Nvar(loc,s) -> fst (dbize_ref k sigma env loc s lvar)
 	  
    (*
    | Slam(_,ona,Node(_,"V$",l)) ->
        let na =
          (match ona with Some s -> Name (id_of_string s) | _ -> Anonymous)
-       in DLAMV(na,Array.of_list (List.map (dbrec (add_rel (na,()) env)) l))
+       in DLAMV(na,Array.of_list (List.map (dbrec (Idset.add na env)) l))
 
    | Slam(_,ona,t) ->
        let na =
          (match ona with Some s -> Name (id_of_string s) | _ -> Anonymous)
-       in DLAM(na, dbrec (add_rel (na,()) env) t)
+       in DLAM(na, dbrec (Idset.add na env) t)
    *)
     | Node(loc,"FIX", (Nvar (locid,iddef))::ldecl) ->
 	let (lf,ln,lA,lt) = dbize_fix ldecl in
@@ -293,7 +297,7 @@ let dbize k sigma env allow_soapp lvar =
           with Not_found ->
 	    error_fixname_unbound "dbize (FIX)" false locid iddef in
 	let ext_env =
-	  List.fold_left (fun env fid -> add_rel (Name fid,()) env) env lf in
+	  List.fold_left (fun env fid -> Idset.add fid env) env lf in
 	let defl = Array.of_list (List.map (dbrec ext_env) lt) in
 	let arityl = Array.of_list (List.map (dbrec env) lA) in
 	RRec (loc,RFix (Array.of_list ln,n), Array.of_list lf, arityl, defl)
@@ -306,17 +310,17 @@ let dbize k sigma env allow_soapp lvar =
           with Not_found ->
 	    error_fixname_unbound "dbize (COFIX)" true locid iddef in
 	let ext_env =
-	  List.fold_left (fun env fid -> add_rel (Name fid,()) env) env lf in
+	  List.fold_left (fun env fid -> Idset.add fid env) env lf in
 	let defl = Array.of_list (List.map (dbrec ext_env) lt) in
 	let arityl = Array.of_list (List.map (dbrec env) lA) in
 	RRec (loc,RCofix n, Array.of_list lf, arityl, defl)
 	  
     | Node(loc,("PROD"|"LAMBDA" as k), [c1;Slam(_,ona,c2)]) ->
-	let na = match ona with
-	  | Some s -> Name (id_of_string s)
-	  | _ -> Anonymous in
+	let na,env' = match ona with
+	  | Some s -> let id = id_of_string s in Name id, Idset.add id env
+	  | _ -> Anonymous, env in
 	let kind = if k="PROD" then BProd else BLambda in
-	RBinder(loc, kind, na, dbrec env c1, dbrec (add_rel (na,()) env) c2)
+	RBinder(loc, kind, na, dbrec env c1, dbrec env' c2)
 
     | Node(_,"PRODLIST", [c1;(Slam _ as c2)]) -> 
 	iterated_binder BProd 0 c1 env c2
@@ -326,11 +330,7 @@ let dbize k sigma env allow_soapp lvar =
     | Node(loc,"APPLISTEXPL", f::args) ->
 	RApp (loc,dbrec env f,List.map (dbrec env) args)
     | Node(loc,"APPLIST", Nvar(locs,s)::args) ->
-	let (c, impargs) =
-          if List.mem s lvar then
-            RRef(loc,RVar (id_of_string s)),[]
-          else
-            dbize_ref k sigma env locs s
+	let (c, impargs) = dbize_ref k sigma env locs s lvar
         in
 	  RApp (loc, c, dbize_args env impargs args)
     | Node(loc,"APPLIST", f::args) ->	   
@@ -393,18 +393,20 @@ let dbize k sigma env allow_soapp lvar =
 	check_uppercase loc ids;
 	check_number_of_pattern loc n pl;
 	let env' =
-	  List.fold_left (fun env id -> add_rel (Name id,()) env) env ids in
+	  List.fold_left (fun env id -> Idset.add id env) env ids in
 	(ids,pl,dbrec env' rhs)
     | _ -> anomaly "dbize: badly-formed ast for Cases equation"
 
   and iterated_binder oper n ty env = function
     | Slam(loc,ona,body) ->
-	let na = match ona with 
-	  | Some s -> check_capture s ty body; Name (id_of_string s) 
-	  | _ -> Anonymous
+	let na,env' = match ona with 
+	  | Some s ->
+	      check_capture s ty body;
+	      let id = id_of_string s in Name id, Idset.add id env
+	  | _ -> Anonymous, env
 	in
 	RBinder(loc, oper, na, dbrec env ty,
-		(iterated_binder oper n ty (add_rel (na,()) env) body))
+		(iterated_binder oper n ty env' body))
     | body -> dbrec env body
 
   and dbize_args env l args =
@@ -434,16 +436,23 @@ let dbize k sigma env allow_soapp lvar =
  * and translates a command to a constr. *)
 
 (*Takes a list of variables which must not be globalized*)
+let from_list l = List.fold_right Idset.add l Idset.empty
+
 let interp_rawconstr_gen sigma env allow_soapp lvar com =
-  dbize CCI sigma (unitize_env (context env)) allow_soapp lvar com
+  dbize CCI sigma
+    (from_list (ids_of_rel_context (rel_context env)))
+    allow_soapp (lvar,var_context env) com
 
 let interp_rawconstr sigma env com =
   interp_rawconstr_gen sigma env false [] com
 
 (*The same as interp_rawconstr but with a list of variables which must not be
   globalized*)
+
 let interp_rawconstr_wo_glob sigma env lvar com =
-  dbize CCI sigma (unitize_env (context env)) false lvar com
+  dbize CCI sigma
+    (from_list (ids_of_rel_context (rel_context env)))
+    false (lvar,var_context env) com
 
 (*let raw_fconstr_of_com sigma env com =
   dbize_fw sigma (unitize_env (context env)) [] com
@@ -460,7 +469,7 @@ let ast_adjust_consts sigma = (* locations are kept *)
 	(let id = id_of_string s in
 	 if Ast.isMeta s then 
 	   ast
-	 else if List.mem id (ids_of_env env) then 
+	 else if Idset.mem id env then 
 	   ast
 	 else 
 	   try 
@@ -481,10 +490,10 @@ let ast_adjust_consts sigma = (* locations are kept *)
 	     with Not_found -> 
 	       warning ("Could not globalize "^s); ast)
 
-    | Slam(loc,None,t) -> Slam(loc,None,dbrec (add_rel (Anonymous,()) env) t)
+    | Slam(loc,None,t) -> Slam(loc,None,dbrec env t)
 	 
     | Slam(loc,Some na,t) ->
-	let env' = add_rel (Name (id_of_string na),()) env in
+	let env' = Idset.add (id_of_string na) env in
         Slam(loc,Some na,dbrec env' t)
     | Node(loc,opn,tl) -> Node(loc,opn,List.map (dbrec env) tl)
     | x -> x
@@ -493,7 +502,7 @@ let ast_adjust_consts sigma = (* locations are kept *)
 
 let globalize_command ast =
   let sign = Global.var_context () in
-  ast_adjust_consts Evd.empty (gLOB sign) ast
+  ast_adjust_consts Evd.empty (from_list (ids_of_var_context sign)) ast
 
 (* Avoid globalizing in non command ast for tactics *)
 let rec glob_ast sigma env = function 
@@ -502,16 +511,16 @@ let rec glob_ast sigma env = function
   | Node(loc,"COMMANDLIST",l) -> 
       Node(loc,"COMMANDLIST", List.map (ast_adjust_consts sigma env) l)
   | Slam(loc,None,t) ->
-      Slam(loc,None,glob_ast sigma (add_rel (Anonymous,()) env) t)
+      Slam(loc,None,glob_ast sigma env t)
   | Slam(loc,Some na,t) ->
-      let env' = add_rel (Name (id_of_string na),()) env in
+      let env' = Idset.add (id_of_string na) env in
       Slam(loc,Some na, glob_ast sigma env' t)
   | Node(loc,opn,tl) -> Node(loc,opn,List.map (glob_ast sigma env) tl)
   | x -> x
 
 let globalize_ast ast =
   let sign = Global.var_context () in
-  glob_ast Evd.empty (gLOB sign) ast
+  glob_ast Evd.empty (from_list (ids_of_var_context sign)) ast
 
 
 (* Installation of the AST quotations. "command" is used by default. *)
@@ -692,8 +701,10 @@ let pattern_of_rawconstr lvar c =
 
 let interp_constrpattern_gen sigma env lvar com = 
   let c =
-    dbize CCI sigma (unitize_env (context env)) true (List.map (fun x ->
-      string_of_id (fst x)) lvar) com
+    dbize CCI sigma (from_list (ids_of_rel_context (rel_context env)))
+      true (List.map
+	      (fun x ->
+		 string_of_id (fst x)) lvar,var_context env) com
   and nlvar = List.map (fun (id,c) -> (id,pattern_of_constr c)) lvar in
   try 
     pattern_of_rawconstr nlvar c
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 9d189edfce..28c4cb3a9f 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -42,9 +42,8 @@ let print_basename_mind sp mindid =
 let print_closed_sections = ref false
 
 let print_typed_value_in_env env (trm,typ) =
-  let sign = Environ.var_context env in
-  [< prterm_env (gLOB sign) trm ; 'fNL ;
-     'sTR "     : "; prtype_env (gLOB sign) typ ; 'fNL >]
+  [< prterm_env env trm ; 'fNL ;
+     'sTR "     : "; prtype_env env typ ; 'fNL >]
 
 let print_typed_value x = print_typed_value_in_env (Global.env ()) x
 
@@ -80,30 +79,22 @@ let print_impl_args = function
    the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u)
    synthesizes the type nat of the abstraction on u *)
 
-let print_var name typ =
+let print_var_def name body typ =
+  [< 'sTR "*** [" ; 'sTR name ; 'sPC; 
+     hOV 0 [< 'sTR "="; prterm body; 'sPC; 'sTR ": "; prtype typ >] ;
+     'sTR "]"; 'fNL >]
+
+let print_var_decl name typ =
   [< 'sTR "*** [" ; 'sTR name ; 'sTR " : "; prtype typ; 'sTR "]"; 'fNL >]
 
-let print_env pk = 
-  let pterminenv = (* if pk = FW then fprterm_env else *) prterm_env in
-  let pr_binder env (na,c) =
-    match na with
-      | Name id as name ->
-          let pc = pterminenv env c in [< print_id id; 'sTR":"; pc >]
-      | Anonymous -> anomaly "Anonymous variables in inductives" 
-  in
-  let rec prec env = function
-    | [] -> [<>] 
-    | [b] -> pr_binder env b
-    | b::rest ->
-        let pb = pr_binder env b in
-        let penvtl = prec (add_rel b env) rest in
-        [< pb; 'sTR";"; 'sPC; penvtl >]
-  in 
-  prec (gLOB nil_sign)
+let print_var (id,c,typ) =
+  let s = string_of_id id in
+  match c with
+    | Some body -> print_var_def s body typ
+    | None -> print_var_decl s typ
 
 let assumptions_for_print lna =
-  List.fold_right (fun na env -> add_rel (na,()) env) lna
-    (ENVIRON(nil_sign,nil_dbsign))
+  List.fold_right (fun na env -> add_name na env) lna empty_names_context
 
 let implicit_args_id id l = 
   if l = [] then 
@@ -126,26 +117,24 @@ let implicit_args_msg sp mipv =
 
 let print_mutual sp mib = 
   let pk = kind_of_path sp in
-  let pterm,pterminenv = pkprinters pk in
   let env = Global.env () in
   let evd = Evd.empty in
   let {mind_packets=mipv; mind_nparams=nparams} = mib in 
   let (lpars,_) = decomp_n_prod env evd nparams (mind_user_arity mipv.(0)) in
-  let lparsname = List.map fst lpars in
-  let lna = Array.map (fun mip -> Name mip.mind_typename) mipv in
-  let lparsprint = assumptions_for_print lparsname in
-  let prass ass_name (id,c) =
-    let pc = pterminenv ass_name c in [< print_id id; 'sTR " : "; pc >] 
+  let arities = Array.map (fun mip -> (Name mip.mind_typename, None, mip.mind_nf_arity)) mipv in
+  let env_ar = push_rels lpars env in
+  let env_cstr = push_rels lpars (push_rels (Array.to_list arities) env) in
+  let pr_constructor (id,c) =
+    let pc = prterm_env env_cstr c in [< print_id id; 'sTR " : "; pc >] 
   in
   let print_constructors mip =
     let lC = mind_user_lc mip in
-    let ass_name = assumptions_for_print (lparsname@(Array.to_list lna)) in
     let lidC =
       Array.to_list 
         (array_map2 (fun id c -> (id,snd (decomp_n_prod env evd nparams c)))
            mip.mind_consnames lC) in
     let plidC = prlist_with_sep (fun () -> [<'bRK(1,0); 'sTR "| " >])
-                  (prass ass_name) lidC in
+                  pr_constructor lidC in
     (hV 0 [< 'sTR "  "; plidC >]) 
   in
   let print_oneind mip = 
@@ -156,9 +145,8 @@ let print_mutual sp mib =
 		  if nparams = 0 then 
 		    [<>] 
 		  else
-		    [< 'sTR "["; print_env pk (List.rev lpars); 
-		       'sTR "]"; 'bRK(1,2) >]; 
-	          'sTR ": "; pterminenv lparsprint arity; 'sTR " :=" >]);
+		    [< 'sTR "["; pr_rel_context env lpars; 'sTR "]"; 'bRK(1,2) >]; 
+	          'sTR ": "; prterm_env env_ar arity; 'sTR " :=" >]);
             'bRK(1,2); print_constructors mip >]) 
   in 
   let mip = mipv.(0) in
@@ -170,8 +158,8 @@ let print_mutual sp mib =
               if nparams = 0 then 
 		[<>] 
               else 
-		[< 'sTR" ["; print_env pk (List.rev lpars); 'sTR "]">];
-              'bRK(1,5); 'sTR": "; pterminenv lparsprint arity; 'sTR" :=";
+		[< 'sTR" ["; pr_rel_context env lpars; 'sTR "]">];
+              'bRK(1,5); 'sTR": "; prterm_env env_ar arity; 'sTR" :=";
               'bRK(0,4); print_constructors mip; 'fNL;
               implicit_args_msg sp mipv  >] )
   (* Mutual [co]inductive definitions *)
@@ -211,10 +199,10 @@ let print_extracted_mutual sp =
 	print_mutual fwsp (Global.lookup_mind fwsp)
     | Some a -> fprterm a
 
-let print_variable sp =
-  let (name,typ,_,_) = out_variable sp in
-  let l = implicits_of_var name in
-  [< print_var (string_of_id name) typ; print_impl_args l; 'fNL >]
+let print_section_variable sp =
+  let ((id,_,_) as d,_,_) = out_variable sp in
+  let l = implicits_of_var id in
+  [< print_var d; print_impl_args l; 'fNL >]
 
 let print_constant with_values sep sp =
   let cb = Global.lookup_constant sp in
@@ -251,7 +239,7 @@ let print_leaf_entry with_values sep (sp,lobj) =
   let tag = object_tag lobj in
   match (sp,tag) with
     | (_,"VARIABLE") ->
-	print_variable sp
+	print_section_variable sp
     | (_,("CONSTANT"|"PARAMETER")) ->
 	print_constant with_values sep sp
     | (_,"INDUCTIVE") ->
@@ -332,39 +320,37 @@ let list_filter_vec f vec =
    of the object, the assumptions that will make it possible to print its type,
    and the constr term that represent its type. *)
 
-let print_constructors fn lna mip = 
-  let ass_name = assumptions_for_print lna in
+let print_constructors fn env_ar mip = 
   let _ =
-    array_map2 (fun id c -> fn (string_of_id id) ass_name c)
+    array_map2 (fun id c -> fn (string_of_id id) env_ar c)
     mip.mind_consnames (mind_user_lc mip)
   in ()
 
-let crible (fn : string -> unit assumptions -> constr -> unit) name =
-  let hyps = gLOB (Global.var_context()) in
+let crible (fn : string -> env -> constr -> unit) name =
+  let env = Global.env () in
   let imported = Library.opened_modules() in
   let const = global_reference CCI name in 
   let rec crible_rec = function
     | (spopt,Lib.Leaf lobj)::rest ->
 	(match (spopt,object_tag lobj) with
 	   | (_,"VARIABLE") ->
-	       let (namec,typ,_,_) = out_variable spopt in 
+	       let ((idc,_,typ),_,_) = out_variable spopt in 
                if (head_const (body_of_type typ)) = const then  
-                 fn (string_of_id namec) hyps (body_of_type typ);
+                 fn (string_of_id idc) env (body_of_type typ);
                crible_rec rest
 	   | (sp,("CONSTANT"|"PARAMETER")) ->
 	       let {const_type=typ} = Global.lookup_constant sp in
                if (head_const (body_of_type typ)) = const then
-                 fn (print_basename sp) hyps (body_of_type typ);
+                 fn (print_basename sp) env (body_of_type typ);
                crible_rec rest
 	   | (sp,"INDUCTIVE") -> 
                let mib = Global.lookup_mind sp in 
-	       let lna =
-		 array_map_to_list
-		   (fun mip -> Name mip.mind_typename) mib.mind_packets in
+	       let arities = array_map_to_list (fun mip -> (Name mip.mind_typename, None, mip.mind_nf_arity)) mib.mind_packets in
+	       let env_ar = push_rels arities env in
                (match const with 
 		  | (DOPN(MutInd(sp',tyi),_)) -> 
 		      if sp = objsp_of sp' then
-			print_constructors fn lna
+			print_constructors fn env_ar
 			  (mind_nth_type_packet mib tyi)
 		  | _ -> ());
                crible_rec rest
@@ -423,25 +409,20 @@ let print_name name =
 	| _ -> raise Not_found
     in
     print_leaf_entry true " = " (sp,lobj)
-  with 
-    | Not_found -> 
-	(try 
-	   (match Declare.global_reference CCI name with
-	      | VAR _ ->
-		  let (_,typ) = Global.lookup_var name in 
-		  [< print_var str typ;
-		     try print_impl_args (implicits_of_var name)
-		     with _ -> [<>] >]
-	      | DOPN(Const sp,_) ->
-		  print_constant true " = " sp
-	      | DOPN(MutInd (sp,_),_) ->
-		  print_inductive sp
-	      | DOPN (MutConstruct((sp,_),_),_) ->
-		  print_inductive sp
-	      | _ -> assert false)
-	 with Not_found | Invalid_argument _ -> 
-	   error (str ^ " not a defined object"))
-    | Invalid_argument _ -> error (str ^ " not a defined object")
+  with Not_found -> 
+  try 
+    match fst (Declare.global_operator CCI name) with
+      | Const sp -> print_constant true " = " sp
+      | MutInd (sp,_) -> print_inductive sp
+      | MutConstruct((sp,_),_) -> print_inductive sp
+      | _ -> assert false
+  with Not_found -> 
+  try
+    let (c,typ) = Global.lookup_var name in 
+    [< print_var (name,c,typ);
+       try print_impl_args (implicits_of_var name)
+       with _ -> [<>] >]
+  with Not_found -> error (str ^ " not a defined object")
 
 let print_opaque_name name = 
   let sigma = Evd.empty in
@@ -463,8 +444,8 @@ let print_opaque_name name =
 	  let ty = Typeops.type_of_constructor env sigma cstr in
 	  print_typed_value (x, ty)
       | IsVar id ->
-          let a = snd(lookup_sign id sign) in 
-	  print_var (string_of_id id) a
+          let (c,ty) = lookup_var id env in 
+	  print_var (id,c,ty)
       | _ -> failwith "print_name"
   with Not_found -> 
     error ((string_of_id name) ^ " not declared")
@@ -475,9 +456,9 @@ let print_local_context () =
     | [] -> [< >]
     | (sp,Lib.Leaf lobj)::rest ->
 	if "VARIABLE" = object_tag lobj then
-          let (name,typ,_,_) = out_variable sp in 
+          let (d,_,_) = out_variable sp in 
 	  [< print_var_rec rest;
-             print_var (string_of_id name) typ >]
+             print_var d >]
 	else 
 	  print_var_rec rest
     | _::rest -> print_var_rec rest
diff --git a/parsing/pretty.mli b/parsing/pretty.mli
index e10c53b802..dd7378d416 100644
--- a/parsing/pretty.mli
+++ b/parsing/pretty.mli
@@ -13,13 +13,12 @@ open Environ
 
 (* A Pretty-Printer for the Calculus of Inductive Constructions. *)
 
-val assumptions_for_print : name list -> unit assumptions
+val assumptions_for_print : name list -> names_context
 
 val print_basename : section_path -> string
 val print_basename_mind : section_path -> identifier -> string
 val print_closed_sections : bool ref
 val print_impl_args : int list -> std_ppcmds
-val print_env : path_kind -> (name * constr) list -> std_ppcmds
 val print_context : bool -> Lib.library_segment -> std_ppcmds
 val print_library_entry : bool -> (section_path * Lib.node) -> std_ppcmds
 val print_full_context : unit -> std_ppcmds
@@ -50,7 +49,7 @@ val print_coercions : unit -> std_ppcmds
 val print_path_between : identifier -> identifier -> std_ppcmds
 
 
-val crible : (string -> unit assumptions -> constr -> unit) -> identifier ->
+val crible : (string -> env -> constr -> unit) -> identifier ->
   unit
 val inspect : int -> std_ppcmds
 
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 89bbdb2e9a..da78f8352e 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -86,28 +86,28 @@ let gentermpr gt =
 
 (* [at_top] means ids of env must be avoided in bound variables *)
 let gentermpr_core at_top env t =
-  gentermpr (Termast.ast_of_constr at_top (unitize_env env) t)
+  gentermpr (Termast.ast_of_constr at_top env t)
 
 let prterm_env_at_top env = gentermpr_core true env
 let prterm_env env = gentermpr_core false env
-let prterm = prterm_env (gLOB nil_sign)
+let prterm = prterm_env empty_env
 
 let prtype_env env typ = prterm_env env (incast_type typ)
-let prtype = prtype_env (gLOB nil_sign)
+let prtype = prtype_env empty_env
 
 let prjudge_env env j =
   (prterm_env env j.uj_val, prterm_env env (incast_type j.uj_type))
-let prjudge = prjudge_env (gLOB nil_sign)
+let prjudge = prjudge_env empty_env
 
 (* Plus de "k"...
 let gentermpr k = gentermpr_core false
 let gentermpr_at_top k = gentermpr_core true
 
 let fprterm_env a = gentermpr FW a
-let fprterm = fprterm_env (gLOB nil_sign)
+let fprterm = fprterm_env empty_env
 
 let fprtype_env env typ = fprterm_env env (incast_type typ)
-let fprtype = fprtype_env (gLOB nil_sign)
+let fprtype = fprtype_env empty_env
 *)
 
 let fprterm_env a =
@@ -123,27 +123,23 @@ let fprtype a =
 (* For compatibility *)
 let fterm0 = fprterm_env
 
-let pr_constant env cst = gentermpr (ast_of_constant (unitize_env env) cst)
-let pr_existential env ev = gentermpr (ast_of_existential (unitize_env env) ev)
-let pr_inductive env ind = gentermpr (ast_of_inductive (unitize_env env) ind)
+let pr_constant env cst = gentermpr (ast_of_constant env cst)
+let pr_existential env ev = gentermpr (ast_of_existential env ev)
+let pr_inductive env ind = gentermpr (ast_of_inductive env ind)
 let pr_constructor env cstr =
-  gentermpr (ast_of_constructor (unitize_env env) cstr)
+  gentermpr (ast_of_constructor env cstr)
 
 open Pattern
 let pr_ref_label = function (* On triche sur le contexte *)
-  | ConstNode sp -> pr_constant (Global.context()) (sp,[||])
-  | IndNode sp -> pr_inductive (Global.context()) (sp,[||])
-  | CstrNode sp -> pr_constructor (Global.context()) (sp,[||])
+  | ConstNode sp -> pr_constant (Global.env()) (sp,[||])
+  | IndNode sp -> pr_inductive (Global.env()) (sp,[||])
+  | CstrNode sp -> pr_constructor (Global.env()) (sp,[||])
   | VarNode id -> print_id id
 
 let pr_cases_pattern t = gentermpr (Termast.ast_of_cases_pattern t)
 let pr_rawterm t = gentermpr (Termast.ast_of_rawconstr t)
-let pr_pattern_env env t =
-  gentermpr (Termast.ast_of_pattern (unitize_env env) t)
-let pr_pattern t = pr_pattern_env (gLOB nil_sign) t
-
-(* For compatibility *)
-let term0 = prterm_env
+let pr_pattern_env env t = gentermpr (Termast.ast_of_pattern env t)
+let pr_pattern t = pr_pattern_env empty_names_context t
 
 let rec gentacpr gt =
   Esyntax.genprint default_tacpr tactic_syntax_universe tactic_initial_prec gt
@@ -155,86 +151,87 @@ and default_tacpr = function
 	[< 'sTR s; 'bRK(1,2); hOV 0 (prlist_with_sep pr_spc gentacpr ta) >]
     | gt -> dfltpr gt
 
-let print_decl sign (s,typ) =
-  let ptyp = prterm_env (gLOB sign) (body_of_type typ) in
-  [< print_id s ; 'sTR" : "; ptyp >]
-
-let print_binding env (na,typ) =
-  let ptyp = prterm_env env (body_of_type typ) in
+let pr_var_decl env (id,c,typ) =
+  let pbody = match c with
+    | None ->  [<  >]
+    | Some c ->  [< 'sTR" := "; prterm_env env c >] in
+  let ptyp = [< 'sTR" : "; prtype_env env typ >] in
+  [< print_id id ; hOV 0 [< pbody; ptyp >] >]
+
+let pr_rel_decl env (na,c,typ) =
+  let pbody = match c with
+    | None ->  [<  >]
+    | Some c ->  [< 'sTR" :="; 'sPC; prterm_env env c >] in
+  let ptyp = prtype_env env typ in
   match na with
-    | Anonymous -> [< 'sTR"<>" ; 'sTR" : " ; ptyp >]
-    | Name id -> [< print_id id ; 'sTR" : "; ptyp >]
+    | Anonymous -> [< 'sTR"<>" ; 'sPC; pbody; 'sTR" :"; 'sPC; ptyp >]
+    | Name id -> [< print_id id ; 'sPC; pbody; 'sTR" :"; 'sPC; ptyp >]
 
 
 (* Prints out an "env" in a nice format.  We print out the
  * signature,then a horizontal bar, then the debruijn environment.
  * It's printed out from outermost to innermost, so it's readable. *)
 
-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))
-
-let sign_it_with_i f sign e =
-  let (_,_,e') = 
-    (sign_it (fun id t (i,sign,e) -> (i+1,add_sign (id,t) sign,
-				      f i id t sign e))
-       sign (0,nil_sign,e))
-  in 
-  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))
-
 (* Prints a signature, all declarations on the same line if possible *)
-let pr_sign sign =
-  hV 0 [< (sign_it_with (fun id t sign pps ->
-                           [< pps; 'wS 2; print_decl sign (id,t) >])
-             sign) [< >] >]
+let pr_var_context_of env =
+  hV 0 [< (fold_var_context
+	     (fun env d pps -> [< pps; 'wS 2; pr_var_decl env d >])
+             env) [< >] >]
+
+let pr_rel_context env rel_context =
+  let rec prec env = function
+    | [] -> [<>] 
+    | [b] -> pr_rel_decl env b
+    | b::rest ->
+        let pb = pr_rel_decl env b in
+        let penvtl = prec (push_rel b env) rest in
+        [< pb; 'sTR";"; 'sPC; penvtl >]
+  in 
+  prec env (List.rev rel_context)
 
 (* Prints an env (variables and de Bruijn). Separator: newline *)
-let pr_env env =
+let pr_context_unlimited env =
   let sign_env =
-    sign_it_with
-      (fun id t sign pps ->
-         let pidt =  print_decl sign (id,t) in [< pps; 'fNL; pidt >])
-      (get_globals env) [< >] 
+    fold_var_context
+      (fun env d pps ->
+         let pidt =  pr_var_decl env d in [< pps; 'fNL; pidt >])
+      env [< >] 
   in
   let db_env =
-    dbenv_it_with 
-      (fun na t env pps ->
-         let pnat = print_binding env (na,t) in [< pps; 'fNL; pnat >])
+    fold_rel_context
+      (fun env d pps ->
+         let pnat = pr_rel_decl env d in [< pps; 'fNL; pnat >])
       env [< >]
   in 
   [< sign_env; db_env >]
 
-let pr_ne_env header k = function
-  | ENVIRON (sign,_) as env when isnull_sign sign & isnull_rel_env env -> [< >]
-  | env -> let penv = pr_env env in [< header; penv >]
+let pr_ne_context_of header k env =
+  if Environ.context env = empty_context then [< >]
+  else let penv = pr_context_unlimited env in [< header; penv >]
 
-let pr_env_limit n env =
-  let sign = get_globals env in
-  let lgsign = sign_length sign in
+let pr_context_limit n env =
+  let var_context = Environ.var_context env in
+  let lgsign = List.length var_context in
   if n >= lgsign then 
-    pr_env env
+    pr_context_unlimited env
   else
     let k = lgsign-n in
-    let sign_env =
-      sign_it_with_i
-        (fun i id t sign pps -> 
+    let _,sign_env =
+      fold_var_context
+        (fun env d (i,pps) ->
            if i < k then 
-	     [< pps ;'sTR "." >] 
+	     (i+1, [< pps ;'sTR "." >])
 	   else
-             let pidt = print_decl sign (id,t) in
-	     [< pps ; 'fNL ;
-		'sTR (emacs_str (String.make 1 (Char.chr 253)));
-		pidt >])
-        (get_globals env) [< >] 
+             let pidt = pr_var_decl env d in
+	     (i+1, [< pps ; 'fNL ;
+		      'sTR (emacs_str (String.make 1 (Char.chr 253)));
+		      pidt >]))
+        env (0,[< >]) 
     in
     let db_env =
-      dbenv_it_with
-        (fun na t env pps ->
-           let pnat = print_binding env (na,t) in
+      fold_rel_context
+        (fun env d pps ->
+           let pnat = pr_rel_decl env d in
 	   [< pps; 'fNL;
 	      'sTR (emacs_str (String.make 1 (Char.chr 253)));
 	      pnat >])
@@ -242,6 +239,6 @@ let pr_env_limit n env =
     in 
     [< sign_env; db_env >]
 
-let pr_env_opt env = match Options.print_hyps_limit () with 
-  | None -> hV 0 (pr_env env)
-  | Some n -> hV 0 (pr_env_limit n env)
+let pr_context_of env = match Options.print_hyps_limit () with 
+  | None -> hV 0 (pr_context_unlimited env)
+  | Some n -> hV 0 (pr_context_limit n env)
diff --git a/parsing/printer.mli b/parsing/printer.mli
index ff3179c7d3..67434ee317 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -6,6 +6,7 @@ open Pp
 open Names
 open Term
 open Sign
+open Environ
 open Rawterm
 open Pattern
 (*i*)
@@ -13,40 +14,43 @@ open Pattern
 (* These are the entry points for printing terms, context, tac, ... *)
 val gentacpr  : Coqast.t -> std_ppcmds
 
-val prterm_env      : 'a assumptions -> constr -> std_ppcmds
-val prterm_env_at_top : 'a assumptions -> constr -> std_ppcmds
+val prterm_env      : env -> constr -> std_ppcmds
+val prterm_env_at_top : env -> constr -> std_ppcmds
 val prterm          : constr -> std_ppcmds
-val prtype_env      : 'a assumptions -> typed_type -> std_ppcmds
+val prtype_env      : env -> typed_type -> std_ppcmds
 val prtype          : typed_type -> std_ppcmds
 val prjudge_env     :
-  'a assumptions -> Environ.unsafe_judgment -> std_ppcmds * std_ppcmds
+  env -> Environ.unsafe_judgment -> std_ppcmds * std_ppcmds
 val prjudge         : Environ.unsafe_judgment -> std_ppcmds * std_ppcmds
 
 val pr_rawterm       : Rawterm.rawconstr -> std_ppcmds
 val pr_cases_pattern : Rawterm.cases_pattern -> std_ppcmds
 
-val pr_constant     : 'a assumptions -> constant -> std_ppcmds
-val pr_existential  : 'a assumptions -> existential -> std_ppcmds
-val pr_constructor  : 'a assumptions -> constructor -> std_ppcmds
-val pr_inductive    : 'a assumptions -> inductive -> std_ppcmds
+val pr_constant     : env -> constant -> std_ppcmds
+val pr_existential  : env -> existential -> std_ppcmds
+val pr_constructor  : env -> constructor -> std_ppcmds
+val pr_inductive    : env -> inductive -> std_ppcmds
 val pr_ref_label    : constr_label -> std_ppcmds
 val pr_pattern      : constr_pattern -> std_ppcmds
-val pr_pattern_env  : 'a assumptions -> constr_pattern -> std_ppcmds
+val pr_pattern_env  : names_context -> constr_pattern -> std_ppcmds
 
-val pr_ne_env       : std_ppcmds -> path_kind -> context -> std_ppcmds
+val pr_ne_context_of : std_ppcmds -> path_kind -> env -> std_ppcmds
 
-val pr_sign         : var_context -> std_ppcmds
-val pr_env_opt      : context -> std_ppcmds
+val pr_var_decl     : env -> var_declaration -> std_ppcmds
+val pr_rel_decl     : env -> rel_declaration -> std_ppcmds
 
-val emacs_str       : string -> string
+val pr_var_context_of : env -> std_ppcmds
+val pr_rel_context  : env -> rel_context -> std_ppcmds
+val pr_context_of   : env -> std_ppcmds
 
-(* For compatibility *)
-val term0           : 'a assumptions -> constr -> std_ppcmds
+val emacs_str       : string -> string
 
-val fprterm_env     : 'a assumptions -> constr -> std_ppcmds
+(*i*) 
+val fprterm_env     : env -> constr -> std_ppcmds
 val fprterm         : constr -> std_ppcmds
-val fprtype_env     : 'a assumptions -> typed_type -> std_ppcmds
+val fprtype_env     : env -> typed_type -> std_ppcmds
 val fprtype         : typed_type -> std_ppcmds
 
 (* For compatibility *)
-val fterm0          : 'a assumptions -> constr -> std_ppcmds
+val fterm0          : env -> constr -> std_ppcmds
+(*i*)
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 7c4568af12..ff8222e4ea 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -9,6 +9,7 @@ open Generic
 open Term
 open Inductive
 open Sign
+open Environ
 open Declare
 open Impargs
 open Coqast
@@ -349,7 +350,7 @@ let occur_id env id0 c =
     | DLAMV(_,v)         -> array_exists (occur (n+1)) v
     | Rel p              ->
     	p>n &
-    	(try (fst (lookup_rel (p-n) env) = Name id0)
+    	(try lookup_name_of_rel (p-n) env = Name id0
 	 with Not_found -> false) (* Unbound indice : may happen in debug *)
     | DOP0 _             -> false
   in 
@@ -396,8 +397,6 @@ let global_vars_and_consts t =
   list_uniquize (collect [] t)
     
 let used_of = global_vars_and_consts
-let ids_of_env = Sign.ids_of_env
-
 
 (****************************************************************************)
 (* Tools for printing of Cases                                              *)
@@ -490,14 +489,14 @@ let ids_of_var cl =
 (* Main translation function from constr -> ast *)
 
 let old_bdize at_top env t =
-  let init_avoid = if at_top then ids_of_env env else [] in
+  let init_avoid = if at_top then ids_of_context env else [] in
   let rec bdrec avoid env t = match collapse_appl t with
     (* Not well-formed constructions *)
     | DLAM(na,c) ->
 	(match concrete_name true (*On ne sait pas si prod*)avoid env na c with
            | (Some id,avoid') -> 
 	       slam(Some (string_of_id id),
-                    bdrec avoid' (add_rel (Name id,()) env) c)
+                    bdrec avoid' (add_name (Name id) env) c)
            | (None,avoid') -> 
 	       slam(None,bdrec avoid' env (pop c)))
     | DLAMV(na,cl) ->
@@ -508,14 +507,14 @@ let old_bdize at_top env t =
 	  let id = next_name_away na avoid in 
 	  slam(Some (string_of_id id),
 	       ope("V$", array_map_to_list
-		     (bdrec (id::avoid) (add_rel (Name id,()) env)) cl))
+		     (bdrec (id::avoid) (add_name (Name id) env)) cl))
 	    
     (* Well-formed constructions *)
     | regular_constr -> 
 	(match kind_of_term regular_constr with
 	   | IsRel n ->
 	       (try 
-		  match fst(lookup_rel n env) with
+		  match lookup_name_of_rel n env with
 		    | Name id   -> nvar (string_of_id id)
 		    | Anonymous -> raise Not_found
 		with Not_found -> 
@@ -610,7 +609,7 @@ let old_bdize at_top env t =
 	       let lfi = List.map (fun na -> next_name_away na avoid) lfn in
 	       let def_env = 
 		 List.fold_left
-		   (fun env id -> add_rel (Name id,()) env) env lfi in
+		   (fun env id -> add_name (Name id) env) env lfi in
 	       let def_avoid = lfi@avoid in
 	       let f = List.nth lfi n in
 	       let rec split_lambda binds env avoid = function
@@ -621,7 +620,7 @@ let old_bdize at_top env t =
 		     let id = next_name_away na avoid in
 		     let ast_of_bind = 
 		       ope("BINDER",[ast;nvar (string_of_id id)]) in
-		     let new_env = add_rel (Name id,()) env in
+		     let new_env = add_name (Name id) env in
 		     split_lambda (ast_of_bind::binds) 
 		       new_env (id::avoid) (n-1,b)
 		 | _ -> error "split_lambda" 
@@ -632,7 +631,7 @@ let old_bdize at_top env t =
 		 | (n, DOP2(Prod,t,DLAM(na,b))) ->
 		     let ast = bdrec avoid env t in
 		     let id = next_name_away na avoid in
-		     let new_env = add_rel (Name id,()) env in
+		     let new_env = add_name (Name id) env in
 		     split_product new_env (id::avoid) (n-1,b)
 		 | _ -> error "split_product" 
 	       in
@@ -655,7 +654,7 @@ let old_bdize at_top env t =
 	       let lfi = List.map (fun na -> next_name_away na avoid) lfn in
 	       let def_env =
 		 List.fold_left 
-		   (fun env id -> add_rel (Name id,()) env) env lfi in
+		   (fun env id -> add_name (Name id) env) env lfi in
 	       let def_avoid = lfi@avoid in
 	       let f = List.nth lfi n in
 	       let listdecl =
@@ -684,7 +683,7 @@ let old_bdize at_top env t =
           if not print_underscore or (dependent (Rel 1) b) then x 
           else Anonymous in
            let id = next_name_away x' avoid in
-           let new_env = (add_rel (Name id,()) env) in
+           let new_env = (add_name (Name id) env) in
            let new_avoid = id::avoid in
            let new_nvarlist = (nvar (string_of_id id))::nvarlist in
              buildrec new_nvarlist new_avoid new_env (n-1,b)
@@ -697,7 +696,7 @@ let old_bdize at_top env t =
 	-> (* nommage de la nouvelle variable *)
           let id = next_ident_away (id_of_string "x") avoid in
 	  let new_nvarlist = (nvar (string_of_id id))::nvarlist in
-          let new_env = (add_rel (Name id,()) env) in
+          let new_env = (add_name (Name id) env) in
           let new_avoid = id::avoid in
           let new_b = DOPN(AppL,[|lift 1 b; Rel 1|]) in
             buildrec new_nvarlist new_avoid new_env (n-1,new_b)
@@ -707,8 +706,8 @@ let old_bdize at_top env t =
   and factorize_binder n avoid env oper na ty c =
     let (env2, avoid2,na2) =
       match concrete_name (oper=Lambda) avoid env na c with
-	  (Some id,l') -> add_rel (Name id,()) env, l', Some (string_of_id id) 
-	| (None,l')    -> add_rel (Anonymous,()) env, l', None
+	  (Some id,l') -> add_name (Name id) env, l', Some (string_of_id id) 
+	| (None,l')    -> add_name Anonymous env, l', None
     in
     let (p,body) = match c with
 	DOP2(oper',ty',DLAM(na',c')) 
@@ -720,7 +719,7 @@ let old_bdize at_top env t =
     in (p,slam(na2, body))
 
   in
-    bdrec init_avoid env t
+    bdrec init_avoid (names_of_rel_context env) t
 (* FIN TO EJECT *)
 (******************************************************************)
        
@@ -728,10 +727,11 @@ let ast_of_constr at_top env t =
   let t' =
     if !print_casts then t
     else Reduction.strong (fun _ _ -> strip_outer_cast)
-      Environ.empty_env Evd.empty t in
+      empty_env Evd.empty t in
   try
-    let avoid = if at_top then ids_of_env env else [] in
-    ast_of_raw (Detyping.detype avoid env t')
+    let avoid = if at_top then ids_of_context env else [] in
+    ast_of_raw 
+      (Detyping.detype avoid (names_of_rel_context env) t')
   with Detyping.StillDLAM ->
     old_bdize at_top env t'
 
@@ -744,14 +744,15 @@ let ast_of_inductive env   = ast_of_inductive_ref (ast_of_constr false env)
 let ast_of_constructor env = ast_of_constructor_ref (ast_of_constr false env)
 
 let rec ast_of_pattern env = function
-  | PRef ref -> ast_of_ref (ast_of_constr false env) ref
+  | PRef ref -> ast_of_ref (fun c -> ast_of_raw (Detyping.detype [] env c)) ref
+
   | PRel n ->
-      (try match fst (lookup_rel n env) with
+      (try match lookup_name_of_rel n env with
 	 | Name id   -> ast_of_ident id
 	 | Anonymous ->
 	     anomaly "ast_of_pattern: index to an anonymous variable"
        with Not_found ->
-	 let s = "[REL "^(string_of_int (number_of_rels env - n))^"]"
+	 let s = "[REL "^(string_of_int n)^"]"
 	 in nvar s)
 
   | PApp (f,args) ->
@@ -771,7 +772,7 @@ let rec ast_of_pattern env = function
   | PBinder (BProd,Anonymous,t,c) ->
       ope("PROD",[ast_of_pattern env t; slam(None,ast_of_pattern env c)])
   | PBinder (bk,na,t,c) ->
-      let env' = add_rel (na,()) env in
+      let env' = add_name na env in
       let (n,a) = factorize_binder_pattern
 		    env' 1 bk na (ast_of_pattern env t) c in
       let tag = match bk with
@@ -785,7 +786,7 @@ let rec ast_of_pattern env = function
       ope(tag,[ast_of_pattern env t;a])
 
   | PLet (id,a,t,c) ->
-      let c' = ast_of_pattern (add_rel (Name id,()) env) c in
+      let c' = ast_of_pattern (add_name (Name id) env) c in
       ope("LET",[ast_of_pattern env a; 	slam(Some (string_of_id id),c')])
 		
 
@@ -814,7 +815,7 @@ and factorize_binder_pattern env n oper na aty c =
 	when (oper = oper') & (aty = ast_of_pattern env ty')
 	  & not (na' = Anonymous & oper = BProd)
 	  ->
-	factorize_binder_pattern (add_rel (na',()) env) (n+1) oper na' aty c'
+	factorize_binder_pattern (add_name na' env) (n+1) oper na' aty c'
     | _ -> (n,ast_of_pattern env c)
   in
   (p,slam(stringopt_of_name na, body))
diff --git a/parsing/termast.mli b/parsing/termast.mli
index 7961ee7fbd..4e62177a97 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -5,6 +5,7 @@
 open Names
 open Term
 open Sign
+open Environ
 open Rawterm
 open Pattern
 (*i*)
@@ -14,21 +15,21 @@ open Pattern
 
 val ast_of_cases_pattern : cases_pattern -> Coqast.t
 val ast_of_rawconstr : rawconstr -> Coqast.t
-val ast_of_pattern : unit assumptions -> constr_pattern -> Coqast.t
+val ast_of_pattern : names_context -> constr_pattern -> Coqast.t
 
 (* If [b=true] in [ast_of_constr b env c] then the variables in the first 
    level of quantification clashing with the variables in [env] are renamed *)
 
-val ast_of_constr : bool -> unit assumptions -> constr -> Coqast.t
+val ast_of_constr : bool -> env -> constr -> Coqast.t
 
 (*i C'est bdize qui sait maintenant s'il faut afficher les casts ou pas
 val bdize_no_casts : bool -> unit assumptions -> constr -> Coqast.t
 i*)
 
-val ast_of_constant     : unit assumptions -> constant -> Coqast.t
-val ast_of_existential  : unit assumptions -> existential -> Coqast.t
-val ast_of_constructor  : unit assumptions -> constructor -> Coqast.t
-val ast_of_inductive    : unit assumptions -> inductive -> Coqast.t
+val ast_of_constant     : env -> constant -> Coqast.t
+val ast_of_existential  : env -> existential -> Coqast.t
+val ast_of_constructor  : env -> constructor -> Coqast.t
+val ast_of_inductive    : env -> inductive -> Coqast.t
 
 (* For debugging *)
 val print_implicits : bool ref