portage Astterm (partiellement)

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

15 files changed, 573 insertions, 449 deletions

diff --git a/.depend b/.depend
index 875f63a479..479d2d0e5f 100644
--- a/.depend
+++ b/.depend
@@ -50,8 +50,8 @@ library/redinfo.cmi: kernel/names.cmi kernel/term.cmi
 library/summary.cmi: kernel/names.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/evd.cmi kernel/names.cmi \
-    pretyping/rawterm.cmi kernel/term.cmi 
+parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
+    kernel/names.cmi pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi 
 parsing/coqast.cmi: lib/dyn.cmi 
 parsing/esyntax.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
     lib/pp.cmi 
@@ -278,12 +278,14 @@ library/declare.cmo: kernel/constant.cmi kernel/evd.cmi kernel/generic.cmi \
     library/global.cmi library/impargs.cmi library/indrec.cmi \
     kernel/inductive.cmi library/lib.cmi library/libobject.cmi \
     kernel/names.cmi library/nametab.cmi kernel/reduction.cmi kernel/sign.cmi \
-    kernel/term.cmi kernel/univ.cmi lib/util.cmi library/declare.cmi 
+    library/summary.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
+    library/declare.cmi 
 library/declare.cmx: kernel/constant.cmx kernel/evd.cmx kernel/generic.cmx \
     library/global.cmx library/impargs.cmx library/indrec.cmx \
     kernel/inductive.cmx library/lib.cmx library/libobject.cmx \
     kernel/names.cmx library/nametab.cmx kernel/reduction.cmx kernel/sign.cmx \
-    kernel/term.cmx kernel/univ.cmx lib/util.cmx library/declare.cmi 
+    library/summary.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
+    library/declare.cmi 
 library/global.cmo: kernel/environ.cmi kernel/generic.cmi \
     kernel/inductive.cmi kernel/instantiate.cmi kernel/sign.cmi \
     library/summary.cmi kernel/term.cmi kernel/typing.cmi lib/util.cmi \
@@ -346,16 +348,16 @@ 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 \
     kernel/names.cmx parsing/pcoq.cmi lib/pp.cmx lib/util.cmx parsing/ast.cmi 
-parsing/astterm.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/environ.cmi \
-    kernel/evd.cmi kernel/generic.cmi toplevel/himsg.cmi kernel/names.cmi \
-    parsing/pcoq.cmi lib/pp.cmi parsing/printer.cmi pretyping/rawterm.cmi \
-    kernel/term.cmi parsing/termast.cmi toplevel/vernac.cmi \
-    parsing/astterm.cmi 
-parsing/astterm.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/environ.cmx \
-    kernel/evd.cmx kernel/generic.cmx toplevel/himsg.cmx kernel/names.cmx \
-    parsing/pcoq.cmi lib/pp.cmx parsing/printer.cmx pretyping/rawterm.cmi \
-    kernel/term.cmx parsing/termast.cmx toplevel/vernac.cmx \
-    parsing/astterm.cmi 
+parsing/astterm.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
+    kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi library/global.cmi \
+    library/impargs.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \
+    pretyping/pretyping.cmi pretyping/rawterm.cmi kernel/sign.cmi \
+    kernel/term.cmi lib/util.cmi toplevel/vernac.cmi parsing/astterm.cmi 
+parsing/astterm.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
+    kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx library/global.cmx \
+    library/impargs.cmx kernel/names.cmx parsing/pcoq.cmi lib/pp.cmx \
+    pretyping/pretyping.cmx pretyping/rawterm.cmi kernel/sign.cmx \
+    kernel/term.cmx lib/util.cmx toplevel/vernac.cmx parsing/astterm.cmi 
 parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi parsing/coqast.cmi 
 parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi 
 parsing/esyntax.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
@@ -364,16 +366,20 @@ parsing/esyntax.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmi \
     lib/gmap.cmx lib/gmapl.cmx lib/pp.cmx lib/util.cmx parsing/esyntax.cmi 
 parsing/lexer.cmo: lib/util.cmi parsing/lexer.cmi 
 parsing/lexer.cmx: lib/util.cmx parsing/lexer.cmi 
-parsing/pretty.cmo: kernel/evd.cmi kernel/generic.cmi library/global.cmi \
-    library/impargs.cmi kernel/inductive.cmi library/lib.cmi \
-    library/libobject.cmi library/library.cmi kernel/names.cmi \
-    library/nametab.cmi lib/pp.cmi parsing/printer.cmi kernel/reduction.cmi \
-    kernel/sign.cmi kernel/term.cmi lib/util.cmi parsing/pretty.cmi 
-parsing/pretty.cmx: kernel/evd.cmx kernel/generic.cmx library/global.cmx \
-    library/impargs.cmx kernel/inductive.cmx library/lib.cmx \
-    library/libobject.cmx library/library.cmx kernel/names.cmx \
-    library/nametab.cmx lib/pp.cmx parsing/printer.cmx kernel/reduction.cmx \
-    kernel/sign.cmx kernel/term.cmx lib/util.cmx parsing/pretty.cmi 
+parsing/pretty.cmo: kernel/constant.cmi library/declare.cmi \
+    kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi library/global.cmi \
+    library/impargs.cmi kernel/inductive.cmi kernel/instantiate.cmi \
+    library/lib.cmi library/libobject.cmi library/library.cmi \
+    kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \
+    kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi kernel/typeops.cmi \
+    lib/util.cmi parsing/pretty.cmi 
+parsing/pretty.cmx: kernel/constant.cmx library/declare.cmx \
+    kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx library/global.cmx \
+    library/impargs.cmx kernel/inductive.cmx kernel/instantiate.cmx \
+    library/lib.cmx library/libobject.cmx library/library.cmx \
+    kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \
+    kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx kernel/typeops.cmx \
+    lib/util.cmx parsing/pretty.cmi 
 parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
     parsing/esyntax.cmi parsing/extend.cmi library/global.cmi \
     kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
diff --git a/Makefile b/Makefile
index d4fd64fbd8..5fb8f9ff2a 100644
--- a/Makefile
+++ b/Makefile
@@ -84,6 +84,12 @@ CMX=$(CMO:.cmo=.cmx)
 
 world: minicoq coqtop.byte dev/db_printers.cmo
 
+LINK=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY)  $(PARSING) $(PRETYPING)
+# $(PROOFS) $(TACTICS) $(TOPLEVEL)
+link: $(LINK)
+	ocamlc -o link $(LINK)
+	rm -f link 
+
 kernel: $(KERNEL)
 library: $(LIBRARY)
 proofs: $(PROOFS)
diff --git a/library/declare.ml b/library/declare.ml
index 909895612e..5d7d624121 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -135,12 +135,48 @@ let declare_mind mie =
   push_inductive_names sp mie;
   declare_inductive_implicits sp
 
+(* Syntax constants. *)
+
+let syntax_table = ref (Idmap.empty : constr Idmap.t)
+
+let _ = Summary.declare_summary
+	  "SYNTAXCONSTANT"
+	  { Summary.freeze_function = (fun () -> !syntax_table);
+	    Summary.unfreeze_function = (fun ft -> syntax_table := ft);
+	    Summary.init_function = (fun () -> syntax_table := Idmap.empty) }
+
+let add_syntax_constant id c =
+  syntax_table := Idmap.add id c !syntax_table
+
+let cache_syntax_constant (sp,c) = 
+  add_syntax_constant (basename sp) c;
+  Nametab.push (basename sp) sp
+
+let open_syntax_constant (sp,_) =
+  Nametab.push (basename sp) sp
+
+let (in_syntax_constant, out_syntax_constant) =
+  let od = {
+    cache_function = cache_syntax_constant;
+    load_function = (fun _ -> ());
+    open_function = open_syntax_constant;
+    specification_function = (fun x -> x) } in
+  declare_object ("SYNTAXCONSTANT", od)
+
+let declare_syntax_constant id c =
+  let sp = add_leaf id CCI (in_syntax_constant c) in
+  add_syntax_constant id c;
+  Nametab.push (basename sp) sp
+
+let out_syntax_constant id = Idmap.find id !syntax_table
+
 (* Test and access functions. *)
 
 let is_constant sp = failwith "TODO"
 let constant_strength sp = failwith "TODO"
 
 let is_variable id = failwith "TODO"
+let out_variable sp = failwith "TODO"
 let variable_strength id = failwith "TODO"
 
 (* Global references. *)
@@ -181,6 +217,17 @@ let global_reference kind id =
   let ids = ids_of_sign hyps in
   DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
 
+let global_reference_imps kind id =
+  let c = global_reference kind id in
+  match c with
+    | DOPN (Const sp,_) -> 
+	c, list_of_implicits (constant_implicits sp)
+    | DOPN (MutInd (sp,i),_) -> 
+	c, list_of_implicits (inductive_implicits (sp,i))
+    | DOPN (MutConstruct ((sp,i),j),_) ->
+	c, list_of_implicits (constructor_implicits ((sp,i),j))
+    | _ -> assert false
+
 let is_global id =
   try 
     let osp = Nametab.sp_of_id CCI id in
diff --git a/library/declare.mli b/library/declare.mli
index 1b3b842cfb..c32ce46ac8 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -30,6 +30,8 @@ val declare_mind : mutual_inductive_entry -> unit
 
 val declare_eliminations : section_path -> unit
 
+val declare_syntax_constant : identifier -> constr -> unit
+
 
 (*s Corresponding test and access functions. *)
 
@@ -37,8 +39,11 @@ val is_constant : section_path -> bool
 val constant_strength : section_path -> strength
 
 val is_variable : identifier -> bool
+val out_variable : section_path -> identifier * typed_type * strength
 val variable_strength : identifier -> strength
 
+val out_syntax_constant : identifier -> constr
+
 (*s It also provides a function [global_reference] to construct a global
   constr (a constant, an inductive or a constructor) from an identifier.
   To do so, it first looks for the section path using [Nametab.sp_of_id] and
@@ -47,6 +52,7 @@ val variable_strength : identifier -> strength
 
 val global_operator : section_path -> identifier -> sorts oper * var_context
 val global_reference : path_kind -> identifier -> constr
+val global_reference_imps : path_kind -> identifier -> constr * int list
 
 val is_global : identifier -> bool
 
diff --git a/library/lib.ml b/library/lib.ml
index 07d4049ce7..46a2833f57 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -26,6 +26,8 @@ type library_entry = section_path * node
 
 let lib_stk = ref ([] : (section_path * node) list)
 
+let lib_tab = Hashtbl.create 353
+
 let module_name = ref None
 let path_prefix = ref ([] : string list)
 
@@ -69,7 +71,8 @@ let split_lib sp =
 (* Adding operations. *)
 
 let add_entry sp node =
-  lib_stk := (sp,node) :: !lib_stk
+  lib_stk := (sp,node) :: !lib_stk;
+  Hashtbl.add lib_tab sp node
 
 let anonymous_id = 
   let n = ref 0 in
@@ -77,7 +80,8 @@ let anonymous_id =
 
 let add_anonymous_entry node =
   let sp = make_path (anonymous_id()) OBJ in
-  add_entry sp node
+  add_entry sp node;
+  sp
 
 let add_leaf id kind obj =
   let sp = make_path id kind in
@@ -88,12 +92,16 @@ let add_anonymous_leaf obj =
   add_anonymous_entry (Leaf obj)
 
 let add_frozen_state () =
-  add_anonymous_entry (FrozenState (freeze_summaries()))
+  let _ = add_anonymous_entry (FrozenState (freeze_summaries())) in ()
 
 let contents_after = function
   | None -> !lib_stk
   | Some sp -> let (after,_,_) = split_lib sp in after
 
+let map_leaf sp = 
+  match Hashtbl.find lib_tab sp with
+    | Leaf obj -> obj
+    | _ -> anomaly "Lib.map_leaf: not a leaf"
 
 (* Sections. *)
 
diff --git a/library/lib.mli b/library/lib.mli
index d8b3def299..d87c4573a8 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -26,10 +26,11 @@ type library_entry = section_path * node
   recent ones coming first). *)
 
 val add_leaf : identifier -> path_kind -> obj -> section_path
-val add_anonymous_leaf : obj -> unit
+val add_anonymous_leaf : obj -> section_path
 
 val contents_after : section_path option -> library_segment
 
+val map_leaf : section_path -> obj
 
 (*s Opening and closing a section. *)
 
diff --git a/parsing/ast.ml b/parsing/ast.ml
index 18758d8ae3..75fdd346ec 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -46,6 +46,12 @@ let path_section loc sp =
   let (sl,bn,pk) = repr_path sp in
   Coqast.Path(loc,List.rev(string_of_id bn :: sl), string_of_kind pk)
 
+let section_path sl k =
+  match List.rev sl with
+    | s::pa -> 
+	make_path pa (id_of_string s) (kind_of_string k)
+    | [] -> invalid_arg "section_path"
+
 (* raising located exceptions *)
 let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm))
 let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm))
diff --git a/parsing/ast.mli b/parsing/ast.mli
index 2663837f34..37823e5adc 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -30,6 +30,8 @@ val dynamic : Dyn.t -> Coqast.t
 val set_loc : Coqast.loc -> Coqast.t -> Coqast.t
 
 val path_section : Coqast.loc -> section_path -> Coqast.t
+val section_path : string list -> string -> section_path
+
 
 (* ast destructors *)
 val num_of_ast : Coqast.t -> int
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 3ca214a434..a6fa07f66a 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -1,38 +1,31 @@
 
 (* $Id$ *)
 
-open Std;;
-open Pp;;
-open Names;;
-open Ast;;
-open Vectops;;
-open Generic;;
-open Term;;
-open Environ;;
-open Termenv;;
-open Impuniv;;
-open Himsg;;
-open Multcase_astterm;; 
-open Evd;;
-open More_util;;
-open Rawterm;;
-
-(**  Multcases ... **)
-
-let prpattern k p = Printer.gencompr CCI (Termast.ast_of_pat p)
+open Pp
+open Util
+open Names
+open Sign
+open Generic
+open Term
+open Environ
+open Evd
+open Impargs
+open Rawterm
+open Pretyping
+open Ast
+open Coqast
 
 (* when an head ident is not a constructor in pattern *)
 let mssg_hd_is_not_constructor s =
-    [< 'sTR ("The symbol "^s^" should be a constructor") >]
-;;
+  [< 'sTR ("The symbol "^s^" should be a constructor") >]
 
 (* checking linearity of a list of ids in patterns *)
 let non_linearl_mssg id =
-  [<'sTR "The variable " ; 'sTR(string_of_id id);
-    'sTR " is bound several times in pattern" >] 
+  [< 'sTR "The variable " ; 'sTR(string_of_id id);
+     'sTR " is bound several times in pattern" >] 
 
 let rec has_duplicate = function 
-    [] -> None
+  | [] -> None
   | x::l -> if List.mem x l then (Some x) else has_duplicate l
 
 let check_linearity loc ids =
@@ -41,7 +34,7 @@ let check_linearity loc ids =
     | None -> ()
 
 let mal_formed_mssg () =
-  [<'sTR "malformed macro of multiple case" >];;
+  [<'sTR "malformed macro of multiple case" >]
 
 (* determines if some pattern variable starts with uppercase *)
 let warning_uppercase loc uplid = (* Comment afficher loc ?? *)
@@ -57,7 +50,7 @@ let is_uppercase_var v =
  | _  -> false
 
 let check_uppercase loc ids =
-  let uplid = filter is_uppercase_var ids in
+  let uplid = List.filter is_uppercase_var ids in
   if uplid <> [] then warning_uppercase loc uplid
 
 (* check that the number of pattern matches the number of matched args *)
@@ -92,7 +85,7 @@ let is_known_constructor k env id =
     with (Not_found | UserError _) -> 
       (try  is_constructor (Environ.search_synconst k id) 
        with Not_found -> false)
-;;
+
 
 let rec abs_eqn k env avoid = function
     (v::ids, Slam(_,ona,t)) ->
@@ -105,7 +98,7 @@ let rec abs_eqn k env avoid = function
 	(id'::nids, DLAM(na,nt))
   | ([],t) -> ([],t)
   | _ -> assert false
-;;
+
 
 let rec absolutize_eqn absrec k env = function
     DOP1(XTRA("LAMEQN",ids),lam_eqn) ->
@@ -115,7 +108,7 @@ let rec absolutize_eqn absrec k env = function
       let _ = if uplid <> [] then warning_uppercase uplid in
       DOP1(XTRA("LAMEQN",nids), absrec neqn)
   | _ -> anomalylabstrm "absolutize_eqn" (mal_formed_mssg())
-;;
+
 *)
 (****************************************************************)
 (* Arguments normally implicit in the "Implicit Arguments mode" *)
@@ -146,7 +139,7 @@ let explicitize_appl l args =
  | ([],_) -> (List.rev acc)@args
  | (_,[]) -> (List.rev acc)
 in aux 1 l args []
-;;
+
 
 let absolutize k sigma env constr = 
  let rec absrec env constr = match constr with
@@ -184,7 +177,7 @@ let absolutize k sigma env constr =
   | DLAMV(na,cl)  -> DLAMV(na,Array.map (absrec (add_rel (na,()) env)) cl)
 
  in absrec env constr
-;;
+
 
 (* Fonctions exportées *)
 let absolutize_cci sigma env constr = absolutize CCI sigma env constr
@@ -192,13 +185,14 @@ let absolutize_fw  sigma env constr = absolutize FW  sigma env constr
 *)
 
 let dbize_sp = function
-    Path(loc,sl,s) ->
-      (try section_path sl s
+  | Path(loc,sl,s) ->
+      (try 
+	 section_path sl s
        with Invalid_argument _ | Failure _ ->
          anomaly_loc(loc,"Astterm.dbize_sp",
                      [< 'sTR"malformed section-path" >]))
   | ast -> anomaly_loc(Ast.loc ast,"Astterm.dbize_sp",
-                     [< 'sTR"not a section-path" >]);;
+                     [< 'sTR"not a section-path" >])
 (*
 let dbize_op loc opn pl cl =
     match (opn,pl,cl) with
@@ -243,7 +237,7 @@ let dbize_op loc opn pl cl =
       | (op,_,_) -> anomaly_loc
             (loc,"Astterm.dbize_op",
              [< 'sTR "Unrecognizable constr operator: "; 'sTR op >])
-;;
+
 
 let split_params =
  let rec sprec acc = function
@@ -253,7 +247,7 @@ let split_params =
    | (Path _ as p)::l -> sprec (p::acc) l
    | l -> (List.rev acc,l)
  in sprec []
-;;
+
 *)
 
 let is_underscore id = (id = "_")
@@ -266,13 +260,15 @@ let ident_of_nvar loc s =
     user_err_loc (loc,"ident_of_nvar", [< 'sTR "Unexpected wildcard" >])
   else (id_of_string s)
 
-let ids_of_ctxt = Termast.ids_of_ctxt
+let ids_of_ctxt = array_map_to_list (function VAR id -> id | _ -> assert false)
 
 let maybe_constructor env s =
-  try match Machops.search_reference env (id_of_string s) with 
-      DOPN(MutConstruct (spi,j),cl) -> Some ((spi,j),ids_of_ctxt cl)
-    | _ -> None
-  with Not_found -> None
+  try 
+    match Declare.global_reference CCI (id_of_string s) with 
+      | DOPN(MutConstruct (spi,j),cl) -> Some ((spi,j),ids_of_ctxt cl)
+      | _ -> None
+  with Not_found -> 
+    None
 
 let dbize_ctxt = 
   List.map 
@@ -281,65 +277,70 @@ let dbize_ctxt =
        | _ -> anomaly "Bad ast for local ctxt of a global reference")
 
 let dbize_global loc = function
-  | ("CONST", sp::ctxt)  -> RRef (loc,RConst (dbize_sp sp,dbize_ctxt ctxt))
-  | ("EVAR", sp::ctxt)   -> RRef (loc,REVar (dbize_sp sp,dbize_ctxt ctxt))
-  | ("MUTIND", sp::Num(_,tyi)::ctxt) -> RRef (loc,RInd ((dbize_sp sp, tyi),dbize_ctxt ctxt))
+  | ("CONST", sp::ctxt) -> 
+      RRef (loc,RConst (dbize_sp sp,dbize_ctxt ctxt))
+  | ("EVAR", (Num (_,ev))::ctxt) -> 
+      RRef (loc,REVar (ev,dbize_ctxt ctxt))
+  | ("MUTIND", sp::Num(_,tyi)::ctxt) -> 
+      RRef (loc,RInd ((dbize_sp sp, tyi),dbize_ctxt ctxt))
   | ("MUTCONSTRUCT", sp::Num(_,ti)::Num(_,n)::ctxt) ->
       RRef (loc,RConstruct (((dbize_sp sp,ti),n),dbize_ctxt ctxt))
-  | ("SYNCONST", [sp]) -> search_synconst_path CCI (dbize_sp sp)
-(* | ("ABST", [sp]) -> RRef (loc,Abst (dbize_sp sp)) *)
+  (* | ("SYNCONST", [sp]) -> search_synconst_path CCI (dbize_sp sp) *)
+  (* | ("ABST", [sp]) -> RRef (loc,Abst (dbize_sp sp)) *)
   | _ -> anomaly_loc (loc,"dbize_global",
 		      [< 'sTR "Bad ast for this global a reference">])
 
 let ref_from_constr = function
-  | DOPN (Const sp,ctxt) -> 
-   if is_existential_id (basename sp) 
-   then REVar (sp,ids_of_ctxt ctxt) 
-   else RConst (sp,ids_of_ctxt ctxt)
+  | DOPN (Const sp,ctxt) -> RConst (sp,ids_of_ctxt ctxt)
+  | DOPN (Evar ev,ctxt) -> REVar (ev,ids_of_ctxt ctxt) 
   | DOPN (MutConstruct (spi,j),ctxt) -> RConstruct ((spi,j),ids_of_ctxt ctxt)
   | DOPN (MutInd (sp,i),ctxt) -> RInd ((sp,i),ids_of_ctxt ctxt)
   | VAR id -> RVar id  (* utilisé dans trad pour coe_value (tmp) *)
   | _ -> anomaly "Not a reference"
 
+let error_var_not_found str loc s = 
+  Ast.user_err_loc 
+    (loc,str,
+     [< 'sTR "The variable"; 'sPC; 'sTR s;
+	'sPC ; 'sTR "was not found"; 
+	'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >])
+
 let dbize_ref k sigma env loc s =
   let id = ident_of_nvar loc s in
-  if (is_existential_id id) then
-    match k with
- 	CCI -> 
-	  RRef (loc,ref_from_constr (
-		  Machops.lookup_exist sigma env (evar_of_id k id))),[]
-      | FW  -> error "existentials in fterms not implemented"
-      | OBJ -> anomaly "absolutize_var"
-  else
-  try match lookup_id id env with
-      RELNAME(n,_) -> RRel (loc,n),[]
-    | _ -> RRef(loc,RVar id), (try Vartab.implicits_of_var k id with _ -> [])
+  try 
+    match lookup_id id env with
+      | RELNAME(n,_) -> RRel (loc,n),[]
+      | _ -> 
+	  RRef(loc,RVar id), (try implicits_of_var k id with _ -> [])
   with Not_found ->
-  try let c,il = match k with
-      CCI -> Machops.search_reference1 env id
-    | FW  -> Machops.search_freference1 env id
-    | OBJ -> anomaly "search_ref_cci_fw" in
-    RRef (loc,ref_from_constr c), il
-  with UserError _ ->
-  try (search_synconst k id,[])
-  with Not_found -> error_var_not_found "dbize_ref" loc s
-
-
-let mkLambdaC(x,a,b) = ope("LAMBDA",[a;slam(Some (string_of_id x),b)])
+    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 UserError _ ->
+      try 
+	RRef (loc,ref_from_constr (Declare.out_syntax_constant id)), []
+      with Not_found -> 
+	error_var_not_found "dbize_ref" loc s
+	  
+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))
 let mkProdC (x,a,b) = ope("PROD",[a;slam(Some (string_of_id x),b)])
 let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b))
+
 let destruct_binder = function
-    Node(_,"BINDER",c::idl) ->
+  | Node(_,"BINDER",c::idl) ->
       List.map (fun id -> (id_of_string (nvar_of_ast id),c)) idl
   | _ -> anomaly "BINDER is expected"
-
+	
 let rec dbize_pattern env = function
   | Node(_,"PATTAS",[Nvar (loc,s); p]) ->
       (match name_of_nvar s with
-	  Anonymous -> dbize_pattern env p
-	| Name id   -> 
-	    let (ids,p') = dbize_pattern env p in (id::ids,PatAs (loc,id,p')))
+	 | Anonymous -> dbize_pattern env p
+	 | Name id   -> 
+	     let (ids,p') = dbize_pattern env p in (id::ids,PatAs (loc,id,p')))
   | Node(_,"PATTCONSTRUCT", Nvar(loc,s)::((_::_) as pl)) ->
       (match maybe_constructor env s with
 	 | Some c ->
@@ -349,7 +350,7 @@ let rec dbize_pattern env = function
 	     user_err_loc (loc,"dbize_pattern",mssg_hd_is_not_constructor s))
   | Nvar(loc,s) ->
       (match name_of_nvar s with
-	   Anonymous -> ([], PatVar (loc,Anonymous))
+	 | Anonymous -> ([], PatVar (loc,Anonymous))
 	 | Name id as name -> ([id], PatVar (loc,name)))
   | _ -> anomaly "dbize: badly-formed ast for Cases pattern"
 
@@ -357,27 +358,34 @@ let rec dbize_fix = function
   | [] -> ([],[],[],[])
   | Node(_,"NUMFDECL", [Nvar(_,fi); Num(_,ni); astA; astT])::rest ->
       let (lf,ln,lA,lt) = dbize_fix rest in
-	((id_of_string fi)::lf, (ni-1)::ln, astA::lA, astT::lt)
+      ((id_of_string fi)::lf, (ni-1)::ln, astA::lA, astT::lt)
   | Node(_,"FDECL", [Nvar(_,fi); Node(_,"BINDERS",bl); astA; astT])::rest ->
       let binders = List.flatten (List.map destruct_binder bl) in
       let ni = List.length binders - 1 in
       let (lf,ln,lA,lt) = dbize_fix rest in
-        ((id_of_string fi)::lf, ni::ln, (mkProdCit binders astA)::lA,
-	 (mkLambdaCit binders astT)::lt)
+      ((id_of_string fi)::lf, ni::ln, (mkProdCit binders astA)::lA,
+       (mkLambdaCit binders astT)::lt)
   | _ -> anomaly "FDECL or NUMFDECL is expected"
 
 let rec dbize_cofix = function
   | [] -> ([],[],[])
   | Node(_,"CFDECL", [Nvar(_,fi); astA; astT])::rest -> 
       let (lf,lA,lt) = dbize_cofix rest in
-	((id_of_string fi)::lf, astA::lA, astT::lt)
+      ((id_of_string fi)::lf, astA::lA, astT::lt)
   | _ -> anomaly "CFDECL is expected"
 
+let error_fixname_unbound str is_cofix loc name = 
+  user_err_loc 
+    (loc,"dbize (COFIX)",
+       [< 'sTR "The name"; 'sPC ; 'sTR name ; 
+	  'sPC ; 'sTR "is not bound in the corresponding"; 'sPC ;
+	  'sTR ((if is_cofix then "co" else "")^"fixpoint definition") >])
+       
 let dbize k sigma =
   let rec dbrec env = function
-    Nvar(loc,s) -> fst (dbize_ref k sigma env loc s)
-
-(*
+    | Nvar(loc,s) -> fst (dbize_ref k sigma env loc s)
+	  
+   (*
    | Slam(_,ona,Node(_,"V$",l)) ->
        let na =
          (match ona with Some s -> Name (id_of_string s) | _ -> Anonymous)
@@ -387,115 +395,133 @@ let dbize k sigma =
        let na =
          (match ona with Some s -> Name (id_of_string s) | _ -> Anonymous)
        in DLAM(na, dbrec (add_rel (na,()) env) t)
-*)
-   | Node(loc,"FIX", (Nvar (locid,iddef))::ldecl) ->
-       let (lf,ln,lA,lt) = dbize_fix ldecl in
-       let n =
-	 try (index (ident_of_nvar locid iddef) lf) -1
-         with Failure _ ->
-	   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
-       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)
-
-   | Node(loc,"COFIX", (Nvar(locid,iddef))::ldecl) ->
-       let (lf,lA,lt) = dbize_cofix ldecl in
-       let n =
-         try (index (ident_of_nvar locid iddef) lf) -1
-         with Failure _ ->
-	   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
-       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 kind = if k="PROD" then BProd else BLambda in
-       RBinder(loc, kind, na, dbrec env c1, dbrec (add_rel (na,()) env) c2)
-   | Node(_,"PRODLIST", [c1;(Slam _ as c2)]) -> iterated_binder BProd c1 env c2
-   | Node(_,"LAMBDALIST", [c1;(Slam _ as c2)]) -> iterated_binder BLambda c1 env c2
-
-   | 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) = dbize_ref k sigma env locs s in
-       RApp (loc, c, dbize_args env impargs args)
-   | Node(loc,"APPLIST", f::args) ->	   
-       RApp (loc,dbrec env f,List.map (dbrec env) args)
-
-   | Node(loc,"MULTCASE", p:: Node(_,"TOMATCH",tms):: eqns) ->
-       let po = match p with Str(_,"SYNTH") -> None | _ -> Some(dbrec env p) in
-       RCases (loc,PrintCases,po,
-	       List.map (dbrec env) tms,
-	       List.map (dbize_eqn (List.length tms) env) eqns)
-
-   | Node(loc,"CASE",Str(_,isrectag)::p::c::cl) ->
-       let po = match p with Str(_,"SYNTH") -> None | _ -> Some(dbrec env p) in
-       let isrec = match isrectag with
-	 | "REC" -> true | "NOREC" -> false 
-	 | _ -> anomaly "dbize: wrong REC tag in CASE" in
-	 ROldCase (loc,isrec,po,dbrec env c,Array.of_list (List.map (dbrec env) cl))
-
-   | Node(loc,"ISEVAR",[]) -> RHole (Some loc)
-   | Node(loc,"META",[Num(_,n)]) -> RRef (loc,RMeta n)
-
-   | Node(loc,"PROP", []) -> RSort(loc,RProp Null)
-   | Node(loc,"SET", [])  -> RSort(loc,RProp Pos)
-   | Node(loc,"TYPE", []) -> RSort(loc,RType)
-
-   (* This case mainly parses things build from   in a quotation *)
-   | Node(loc,("CONST"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),l) ->
-       dbize_global loc (key,l)
-
-   | Node(loc,opn,tl) -> anomaly ("dbize found operator "^opn^" with "^(string_of_int (List.length tl))^" arguments")
-
- | _ -> anomaly "dbize: unexpected ast"
+   *)
+    | Node(loc,"FIX", (Nvar (locid,iddef))::ldecl) ->
+	let (lf,ln,lA,lt) = dbize_fix ldecl in
+	let n =
+	  try 
+	    (list_index (ident_of_nvar locid iddef) lf) -1
+          with Failure _ ->
+	    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
+	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)
+	  
+    | Node(loc,"COFIX", (Nvar(locid,iddef))::ldecl) ->
+	let (lf,lA,lt) = dbize_cofix ldecl in
+	let n =
+          try 
+	    (list_index (ident_of_nvar locid iddef) lf) -1
+          with Failure _ ->
+	    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
+	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 kind = if k="PROD" then BProd else BLambda in
+	RBinder(loc, kind, na, dbrec env c1, dbrec (add_rel (na,()) env) c2)
+
+    | Node(_,"PRODLIST", [c1;(Slam _ as c2)]) -> 
+	iterated_binder BProd c1 env c2
+    | Node(_,"LAMBDALIST", [c1;(Slam _ as c2)]) -> 
+	iterated_binder BLambda c1 env c2
+
+    | 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) = dbize_ref k sigma env locs s in
+	RApp (loc, c, dbize_args env impargs args)
+    | Node(loc,"APPLIST", f::args) ->	   
+	RApp (loc,dbrec env f,List.map (dbrec env) args)
+	  
+    | Node(loc,"MULTCASE", p:: Node(_,"TOMATCH",tms):: eqns) ->
+	let po = match p with 
+	  | Str(_,"SYNTH") -> None 
+	  | _ -> Some(dbrec env p) in
+	RCases (loc,PrintCases,po,
+		List.map (dbrec env) tms,
+		List.map (dbize_eqn (List.length tms) env) eqns)
+
+    | Node(loc,"CASE",Str(_,isrectag)::p::c::cl) ->
+	let po = match p with 
+	  | Str(_,"SYNTH") -> None 
+	  | _ -> Some(dbrec env p) in
+	let isrec = match isrectag with
+	  | "REC" -> true | "NOREC" -> false 
+	  | _ -> anomaly "dbize: wrong REC tag in CASE" in
+	ROldCase (loc,isrec,po,dbrec env c,
+		  Array.of_list (List.map (dbrec env) cl))
+
+    | Node(loc,"ISEVAR",[]) -> RHole (Some loc)
+    | Node(loc,"META",[Num(_,n)]) -> RRef (loc,RMeta n)
+
+    | Node(loc,"PROP", []) -> RSort(loc,RProp Null)
+    | Node(loc,"SET", [])  -> RSort(loc,RProp Pos)
+    | Node(loc,"TYPE", []) -> RSort(loc,RType)
+	  
+    (* This case mainly parses things build from   in a quotation *)
+    | Node(loc,("CONST"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),l) ->
+	dbize_global loc (key,l)
+
+    | Node(loc,opn,tl) -> 
+	anomaly ("dbize found operator "^opn^" with "^
+		 (string_of_int (List.length tl))^" arguments")
+
+    | _ -> anomaly "dbize: unexpected ast"
 
   and dbize_eqn n env = function
-  | Node(loc,"EQN",rhs::lhs) ->
-      let (idsl,pl) = List.split (List.map (dbize_pattern env) lhs) in
-      let ids = List.flatten idsl in
-      check_linearity loc ids;
-      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
+    | Node(loc,"EQN",rhs::lhs) ->
+	let (idsl,pl) = List.split (List.map (dbize_pattern env) lhs) in
+	let ids = List.flatten idsl in
+	check_linearity loc ids;
+	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
 	(ids,pl,dbrec env' rhs)
-  | _ -> anomaly "dbize: badly-formed ast for Cases equation"
+    | _ -> anomaly "dbize: badly-formed ast for Cases equation"
 
   and iterated_binder oper ty env = function
-    Slam(loc,ona,body) ->
-      let na =
-        (match ona with Some s -> Name (id_of_string s) | _ -> Anonymous)
-      in RBinder(loc, oper, na, 
-		 dbrec (add_rel (Anonymous,()) env) ty, (* To avoid capture *)
-		 (iterated_binder oper ty (add_rel (na,()) env) body))
-  | body -> dbrec env body
-
+    | Slam(loc,ona,body) ->
+	let na =match ona with 
+	  | Some s -> Name (id_of_string s) 
+	  | _ -> Anonymous
+	in 
+	RBinder(loc, oper, na, 
+		dbrec (add_rel (Anonymous,()) env) ty, (* To avoid capture *)
+		(iterated_binder oper ty (add_rel (na,()) env) body))
+    | body -> dbrec env body
+	  
   and dbize_args env l args =
-  let rec aux n l args = match (l,args) with 
-    | (i::l',Node(loc, "EXPL", [Num(_,j);a])::args') ->
-	if i=n & j>=i then
-	  if j=i
-	  then (dbrec env a)::(aux (n+1) l' args')
-	  else (RHole None)::(aux (n+1) l' args)
-	else error "Bad explicitation number"
-    | (i::l',a::args') -> 
-	if i=n
-	then (RHole None)::(aux (n+1) l' args)
-	else (dbrec env a)::(aux (n+1) l' args')
-    | ([],args) -> List.map (dbrec env) args
-    | (_,[]) -> []
-  in aux 1 l args
-
-  in dbrec
-;;
+    let rec aux n l args = match (l,args) with 
+      | (i::l',Node(loc, "EXPL", [Num(_,j);a])::args') ->
+	  if i=n & j>=i then
+	    if j=i then 
+	      (dbrec env a)::(aux (n+1) l' args')
+	    else 
+	      (RHole None)::(aux (n+1) l' args)
+	  else 
+	    error "Bad explicitation number"
+      | (i::l',a::args') -> 
+	  if i=n then 
+	    (RHole None)::(aux (n+1) l' args)
+	  else 
+	    (dbrec env a)::(aux (n+1) l' args')
+      | ([],args) -> List.map (dbrec env) args
+      | (_,[]) -> []
+    in 
+    aux 1 l args
+
+  in 
+  dbrec
 
 (*
 let dbize_kind ... =
@@ -516,7 +542,7 @@ let dbize_kind ... =
          [< 'sTR"During the relocation of global references," >], e,
          [< 'sTR"Perhaps the input is malformed" >])
   in c
-;;
+
 *)
 
 let dbize_cci sigma env com = dbize CCI sigma env com
@@ -528,17 +554,17 @@ let dbize_fw  sigma env com = dbize FW sigma env com
 let raw_constr_of_com sigma env com =
   let c = dbize_cci sigma (unitize_env env) com in
     try Sosub.soexecute c
-    with Failure _|UserError _ -> error_sosub_execute CCI com;;
+    with Failure _|UserError _ -> error_sosub_execute CCI com
 
 let raw_fconstr_of_com sigma env com =
   let c = dbize_fw sigma (unitize_env env) com in
     try Sosub.soexecute c
-    with Failure _|UserError _ -> error_sosub_execute FW com;;
+    with Failure _|UserError _ -> error_sosub_execute FW com
 
 let raw_constr_of_compattern sigma env com =
   let c = dbize_cci sigma (unitize_env env) com in
     try Sosub.try_soexecute c
-    with Failure _|UserError _ -> error_sosub_execute CCI com;;
+    with Failure _|UserError _ -> error_sosub_execute CCI com
  *)
 
 let raw_constr_of_com sigma env com = dbize_cci sigma (unitize_env env) com
@@ -551,42 +577,46 @@ let raw_constr_of_compattern sigma env com =
    to get statically bound idents in grammar or pretty-printing rules) *)
 
 let ast_adjust_consts sigma = (* locations are kept *)
- let rec dbrec env = function
-    Nvar(loc,s) as ast ->
-      (let id = id_of_string s in
-      if (Ast.isMeta s) or (is_existential_id id) then ast
-      else if List.mem id (ids_of_env env) then ast
-      else 
-      try match Machops.search_reference env id with
-	| DOPN (Const sp,_) -> 
-	    if is_existential_id (basename sp) 
-	    then Node(loc,"EVAR",[path_section loc sp])
-	    else Node(loc,"CONST",[path_section loc sp])
-	| DOPN (MutConstruct ((sp,i),j),_) ->
-	    Node (loc,"MUTCONSTRUCT",[path_section loc sp;num i;num j])
-	| DOPN (MutInd (sp,i),_) ->
-	    Node (loc,"MUTIND",[path_section loc sp;num i])
-	| _ -> anomaly "Not a reference"
-      with UserError _ | Not_found ->
-      try let _ = search_synconst CCI id in Node(loc,"SYNCONST",[Nvar(loc,s)])
-      with Not_found -> warning ("Could not globalize "^s); ast)
-
-   | Slam(loc,None,t) -> Slam(loc,None,dbrec (add_rel (Anonymous,()) env) t)
-
-   | Slam(loc,Some na,t) ->
-       let env' = add_rel (Name (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
- in dbrec
-;;
-
+  let rec dbrec env = function
+    | Nvar(loc,s) as ast ->
+	(let id = id_of_string s in
+	 if Ast.isMeta s then 
+	   ast
+	 else if List.mem id (ids_of_env env) then 
+	   ast
+	 else 
+	   try 
+	     match Declare.global_reference CCI id with
+	       | DOPN (Const sp,_) -> 
+		   Node(loc,"CONST",[path_section loc sp])
+	       | DOPN (Evar ev,_) ->
+		   Node(loc,"EVAR",[Num(loc,ev)])
+	       | DOPN (MutConstruct ((sp,i),j),_) ->
+		   Node (loc,"MUTCONSTRUCT",[path_section loc sp;num i;num j])
+	       | DOPN (MutInd (sp,i),_) ->
+		   Node (loc,"MUTIND",[path_section loc sp;num i])
+	       | _ -> anomaly "Not a reference"
+	   with UserError _ | Not_found ->
+	     try 
+	       let _ = Declare.out_syntax_constant id in 
+	       Node(loc,"SYNCONST",[Nvar(loc,s)])
+	     with Not_found -> 
+	       warning ("Could not globalize "^s); ast)
+
+    | Slam(loc,None,t) -> Slam(loc,None,dbrec (add_rel (Anonymous,()) env) t)
+	 
+    | Slam(loc,Some na,t) ->
+	let env' = add_rel (Name (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
+  in 
+  dbrec
 
 let globalize_command ast =
-  let (sigma,sign) = Termenv.initial_sigma_sign() in
-    ast_adjust_consts sigma (gLOB sign) ast
-;;
-
+  let env = Global.unsafe_env () in
+  let sign = get_globals (Environ.context env) in
+  ast_adjust_consts Evd.empty (gLOB sign) ast
 
 (* Avoid globalizing in non command ast for tactics *)
 let rec glob_ast sigma env = function 
@@ -598,21 +628,25 @@ let rec glob_ast sigma env = function
       Slam(loc,None,glob_ast sigma (add_rel (Anonymous,()) env) t)
   | Slam(loc,Some na,t) ->
       let env' = add_rel (Name (id_of_string na),()) env in
-        Slam(loc,Some na, glob_ast sigma env' t)
+      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 (sigma,sign) = Termenv.initial_sigma_sign() in
-    glob_ast sigma (gLOB sign) ast
-;;
+  let env = Global.unsafe_env () in
+  let sign = get_globals (Environ.context env) in
+  glob_ast Evd.empty (gLOB sign) ast
+
 
 (* Installation of the AST quotations. "command" is used by default. *)
-open Pcoq;;
-define_quotation true "command" (map_entry globalize_command Command.command);;
-define_quotation false "tactic" (map_entry globalize_ast Tactic.tactic);;
-define_quotation false "vernac" (map_entry globalize_ast Vernac.vernac);;
+open Pcoq
+
+let _ = 
+  define_quotation true "command" (map_entry globalize_command Command.command)
+let _ = 
+  define_quotation false "tactic" (map_entry globalize_ast Tactic.tactic)
+let _ = 
+  define_quotation false "vernac" (map_entry globalize_ast Vernac.vernac)
 
 
 (*********************************************************************)
@@ -622,43 +656,46 @@ define_quotation false "vernac" (map_entry globalize_ast Vernac.vernac);;
 
 (* With dB *)
 
-let constr_of_com_env1 is_ass sigma hyps com = 
-  let c = Astterm.raw_constr_of_com sigma hyps com in
-  try ise_resolve1 is_ass sigma hyps c
-  with e -> Stdpp.raise_with_loc (Ast.loc com) e
-
-
-let constr_of_com_env sigma hyps com =
-  constr_of_com_env1 false sigma hyps com
-
-let fconstr_of_com_env1 is_ass  sigma hyps com = 
-  let c = Astterm.raw_fconstr_of_com sigma hyps com in
-    try ise_resolve1 is_ass sigma hyps c
-    with e -> Stdpp.raise_with_loc (Ast.loc com) e
-
+let constr_of_com_env1 is_ass sigma env com = 
+  let c = raw_constr_of_com sigma (context env) com in
+  try 
+    ise_resolve1 is_ass sigma env c
+  with e -> 
+    Stdpp.raise_with_loc (Ast.loc com) e
+
+let constr_of_com_env sigma env com =
+  constr_of_com_env1 false sigma env com
+    
+let fconstr_of_com_env1 is_ass sigma env com = 
+  let c = raw_fconstr_of_com sigma (context env) com in
+  try 
+    ise_resolve1 is_ass sigma env c
+  with e -> 
+    Stdpp.raise_with_loc (Ast.loc com) e
  
 let fconstr_of_com_env sigma hyps com =
   fconstr_of_com_env1 false sigma hyps com 
-
-
+    
 (* Without dB *)
-let type_of_com sign com =
-  let env = gLOB sign in
-  let c = Astterm.raw_constr_of_com mt_evd env com in
-  try ise_resolve_type true mt_evd [] env c
-  with e -> Stdpp.raise_with_loc (Ast.loc com) e
-
-
-let constr_of_com1 is_ass sigma sign com = 
-  constr_of_com_env1 is_ass sigma (gLOB sign) com
+let type_of_com env com =
+  let sign = context env in
+  let c = raw_constr_of_com Evd.empty sign com in
+  try 
+    ise_resolve_type true Evd.empty [] env c
+  with e -> 
+    Stdpp.raise_with_loc (Ast.loc com) e
+
+let constr_of_com1 is_ass sigma env com = 
+  constr_of_com_env1 is_ass sigma env com
+    
+let constr_of_com sigma env com =
+  constr_of_com1 false sigma env com
 
-let constr_of_com sigma sign com =
-  constr_of_com1 false sigma sign com
 let constr_of_com_sort sigma sign com =
   constr_of_com1 true sigma sign com
 
-let fconstr_of_com1 is_ass sigma sign com = 
-  fconstr_of_com_env1 is_ass sigma (gLOB sign) com
+let fconstr_of_com1 is_ass sigma env com = 
+  fconstr_of_com_env1 is_ass sigma env com
 
 let fconstr_of_com sigma sign com  =
   fconstr_of_com1 false sigma sign com
@@ -666,40 +703,43 @@ let fconstr_of_com_sort sigma sign com  =
   fconstr_of_com1 true sigma sign com
 
 (* Note: typ is retyped *)
-let constr_of_com_casted sigma sign com typ = 
-  let env = gLOB sign in
-  let c = Astterm.raw_constr_of_com sigma env com in
+(***
+let constr_of_com_casted sigma env com typ = 
+  let sign = context env in
+  let c = raw_constr_of_com sigma sign com in
   let isevars = ref sigma in
   try
     let j = unsafe_fmachine
 	      (mk_tycon (nf_ise1 sigma typ)) false isevars [] env c in
-    (j_apply (process_evars true !isevars) j)._VAL
-  with e -> Stdpp.raise_with_loc (Ast.loc com) e
-
-
+    (j_apply (process_evars true !isevars) j).uj_val
+  with e -> 
+    Stdpp.raise_with_loc (Ast.loc com) e
 
 (* Typing with Trad, and re-checking with Mach *)
 let fconstruct_type sigma sign com =
-  let c = constr_of_com1 true sigma sign com
-  in Mach.fexecute_type sigma sign c
+  let c = constr_of_com1 true sigma sign com in 
+  Mach.fexecute_type sigma sign c
 
 let fconstruct sigma sign com =
-  let c = constr_of_com1 false sigma sign com
-  in Mach.fexecute sigma sign c
+  let c = constr_of_com1 false sigma sign com in 
+  Mach.fexecute sigma sign c
 
 let infconstruct_type sigma (sign,fsign) cmd =
-  let c = constr_of_com1 true sigma sign cmd
-  in Mach.infexecute_type sigma (sign,fsign) c
+  let c = constr_of_com1 true sigma sign cmd in 
+  Mach.infexecute_type sigma (sign,fsign) c
 
 let infconstruct sigma (sign,fsign) cmd =
-  let c = constr_of_com1 false sigma sign cmd
-  in Mach.infexecute sigma (sign,fsign) c
+  let c = constr_of_com1 false sigma sign cmd in 
+  Mach.infexecute sigma (sign,fsign) c
 
 (* Type-checks a term with the current universe constraints, the resulting
    constraints are dropped. *)
+
 let univ_sp = make_path ["univ"] (id_of_string "dummy") OBJ
+
 let fconstruct_with_univ sigma sign com =
   let c = constr_of_com sigma sign com in
-  let(_,j) = with_universes (Mach.fexecute sigma sign)
-               (univ_sp, Constraintab.current_constraints(), c)
-  in j
+  let (_,j) = with_universes (Mach.fexecute sigma sign)
+		(univ_sp, Constraintab.current_constraints(), c) in 
+  j
+***)
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index e6029cdb72..7c48d28189 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -1,22 +1,16 @@
-(****************************************************************************)
-(*                 The Calculus of Inductive Constructions                  *)
-(*                                                                          *)
-(*                                Projet Coq                                *)
-(*                                                                          *)
-(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
-(*              Rocquencourt         Orsay          Lyon                    *)
-(*                                                                          *)
-(*                                 Coq V6.3                                 *)
-(*                               July 1st 1999                              *)
-(*                                                                          *)
-(****************************************************************************)
-(*                               astterm.mli                                *)
-(****************************************************************************)
 
+(* $Id$ *)
+
+(*i*)
 open Names
 open Term
+open Sign
 open Evd
+open Environ
 open Rawterm
+(*i*)
+
+(* Translation from AST to terms. *)
 
 (*
 val dbize_op : CoqAst.loc -> string -> CoqAst.t list -> constr list -> constr
@@ -24,38 +18,38 @@ val dbize    : unit assumptions -> CoqAst.t -> constr
 
 val absolutize_cci : 'c evar_map -> unit assumptions -> constr -> constr
 *)
-val dbize_cci      : 'c evar_map -> unit assumptions -> CoqAst.t -> rawconstr
+val dbize_cci      : 'c evar_map -> unit assumptions -> Coqast.t -> rawconstr
 
 (*
 val absolutize_fw  : 'c evar_map -> unit assumptions -> constr -> constr
 *)
-val dbize_fw       : 'c evar_map -> unit assumptions -> CoqAst.t -> rawconstr
+val dbize_fw       : 'c evar_map -> unit assumptions -> Coqast.t -> rawconstr
 
 val raw_constr_of_com :
-  'c evar_map -> 'a assumptions -> CoqAst.t -> rawconstr
+  'c evar_map -> 'a assumptions -> Coqast.t -> rawconstr
 val raw_fconstr_of_com :
-  'c evar_map -> 'a assumptions -> CoqAst.t -> rawconstr
+  'c evar_map -> 'a assumptions -> Coqast.t -> rawconstr
 val raw_constr_of_compattern :
-  'c evar_map -> 'a assumptions -> CoqAst.t -> rawconstr
+  'c evar_map -> 'a assumptions -> Coqast.t -> rawconstr
 
-val globalize_command : CoqAst.t -> CoqAst.t
-val globalize_ast     : CoqAst.t -> CoqAst.t
+val globalize_command : Coqast.t -> Coqast.t
+val globalize_ast     : Coqast.t -> Coqast.t
 
 (*i Ceci était avant dans Trad
     Maintenant elles sont là car relève des ast i*)
 
-val type_of_com : context -> Coqast.t -> typed_type
+val type_of_com : unsafe_env -> Coqast.t -> typed_type
 
 val constr_of_com_casted : 'c evar_map -> context -> Coqast.t -> constr ->
   constr
 
-val constr_of_com1 : bool -> 'c evar_map -> context -> Coqast.t -> constr
-val constr_of_com : 'c evar_map -> context -> Coqast.t -> constr
-val constr_of_com_sort : 'c evar_map -> context -> Coqast.t -> constr
+val constr_of_com1 : bool -> 'c evar_map -> unsafe_env -> Coqast.t -> constr
+val constr_of_com : 'c evar_map -> unsafe_env -> Coqast.t -> constr
+val constr_of_com_sort : 'c evar_map -> unsafe_env -> Coqast.t -> constr
 
-val fconstr_of_com1 : bool -> 'c evar_map -> context -> Coqast.t -> constr
-val fconstr_of_com : 'c evar_map -> context -> Coqast.t -> constr
-val fconstr_of_com_sort : 'c evar_map -> context -> Coqast.t -> constr
+val fconstr_of_com1 : bool -> 'c evar_map -> unsafe_env -> Coqast.t -> constr
+val fconstr_of_com : 'c evar_map -> unsafe_env -> Coqast.t -> constr
+val fconstr_of_com_sort : 'c evar_map -> unsafe_env -> Coqast.t -> constr
 
 (* Typing with Trad, and re-checking with Mach *)
 
@@ -65,6 +59,4 @@ val fconstruct_type :
 
 (* Typing, re-checking with universes constraints *)
 val fconstruct_with_univ :
-  'c evar_map -> context -> Coqast.t -> judgement
-
-(* $Id$ *)
+  'c evar_map -> context -> Coqast.t -> unsafe_judgment
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 59d93aaa0a..0588446225 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -6,10 +6,13 @@ open Util
 open Names
 open Generic
 open Term
+open Constant
 open Inductive
 open Sign
-open Printer
 open Reduction
+open Environ
+open Instantiate
+open Declare
 open Impargs
 open Libobject
 open Printer
@@ -38,11 +41,12 @@ let print_basename_mind sp mindid =
 
 let print_closed_sections = ref false
 
-let print_typed_value_in_sign sign (trm,typ) =
+let print_typed_value_in_env env (trm,typ) =
+  let sign = get_globals (Environ.context env) in
   [< term0 (gLOB sign) trm ; 'fNL ;
      'sTR "     : "; term0 (gLOB sign) typ ; 'fNL >]
 
-let print_typed_value = print_typed_value_in_sign nil_sign
+let print_typed_value x = print_typed_value_in_env (Global.unsafe_env()) x
 			  		  
 let print_recipe = function
   | Some c -> prterm c
@@ -123,7 +127,8 @@ let implicit_args_msg sp mipv =
           >])
        mipv >]
 
-let print_mutual pk sp mib = 
+let print_mutual sp mib = 
+  let pk = kind_of_path sp in
   let pterm,pterminenv =
     if pk = FW then (fprterm,fterm0) else (prterm,term0) in
   let env = Global.unsafe_env () in
@@ -206,23 +211,23 @@ let print_extracted_mutual sp =
   match mib.mind_singl with 
     | None -> 
 	let fwsp = fwsp_of sp in
-	print_mutual FW fwsp (Global.lookup_mind fwsp)
+	print_mutual fwsp (Global.lookup_mind fwsp)
     | Some a -> fprterm a
 
 let print_leaf_entry with_values sep (spopt,lobj) =
   let tag = object_tag lobj in
   match (spopt,tag) with
     | (_,"VARIABLE") ->
-	let (name,(typ,_),_,l,_,_) = outVariable lobj in
-	[< print_var (string_of_id name) typ; 
-	   print_impl_args (list_of_implicits l); 'fNL >]
+	let (name,typ,_) = out_variable spopt in
+	let l = implicits_of_var (kind_of_path spopt) name in
+	[< print_var (string_of_id name) typ; print_impl_args l; 'fNL >]
  
     | (sp,"CONSTANT") ->
-	let (cmap,_,_) = outConstant lobj in
-	if Listmap.in_dom cmap CCI then
-	  let {cONSTBODY=val_0;cONSTTYPE=typ;cONSTIMPARGS=l} = 
-	    Listmap.map cmap CCI
-	  in 
+	let cb = Global.lookup_constant sp in
+	if kind_of_path sp = CCI then
+	  let val_0 = cb.const_body in
+	  let typ = cb.const_type in
+	  let l = constant_implicits sp in
 	  hOV 0 [< (match val_0 with 
 		      | None -> 
 			  [< 'sTR"*** [ "; 
@@ -241,25 +246,23 @@ let print_leaf_entry with_values sep (spopt,lobj) =
 		   'sTR (print_basename (fwsp_of sp)) ; 'fNL>]
 
     | (sp,"MUTUALINDUCTIVE") ->
-	let (cmap,_) = outMutualInductive lobj in
-	if Listmap.in_dom cmap CCI then
-	  [< print_mutual CCI (Listmap.map cmap CCI); 'fNL >]
+	let mib = Global.lookup_mind sp in
+	if kind_of_path sp = CCI then
+	  [< print_mutual sp mib; 'fNL >]
 	else
 	  hOV 0 [< 'sTR"Fw inductive definition " ; 
 		   'sTR (print_basename (fwsp_of sp)) ; 'fNL >]
 
-    | (_,"UNIVERSES") -> [< print_universes_object (outUniverses lobj); 'fNL >]
-
     | (_,"AUTOHINT") -> [< 'sTR" Add Auto Marker" ; 'fNL >]
 
     | (_,"GRAMMAR") -> [< 'sTR" Grammar Marker" ; 'fNL >]
 
     | (sp,"SYNTAXCONSTANT") -> 
+	let id = basename sp in
         [< 'sTR" Syntax Macro " ; 
-      	   'sTR(string_of_id(basename sp)) ; 'sTR sep;  
+      	   print_id id ; 'sTR sep;  
            if with_values then 
-             let cmap = outSyntaxConstant lobj in 
-      	     [< prterm (Listmap.map cmap CCI) >]
+             let c = out_syntax_constant id in [< prterm c >]
            else [<>]; 'fNL >]
 	
     | (_,"PPSYNTAX") -> [< 'sTR" Syntax Marker" ; 'fNL >]
@@ -274,20 +277,19 @@ let print_leaf_entry with_values sep (spopt,lobj) =
 let rec print_library_entry with_values ent = 
   let sep = if with_values then " = " else " : " in 
   match ent with
-    | (sp,Lib.LEAF lobj) -> [< print_leaf_entry with_values sep (sp,lobj) >]
-    | (s,Lib.ClosedDir(_,_,_,ctxt)) ->
+    | (sp,Lib.Leaf lobj) -> 
+	[< print_leaf_entry with_values sep (sp,lobj) >]
+    | (s,Lib.ClosedSection(_,ctxt)) ->
 	[< 'sTR"Closed Section " ; 'sTR (string_of_path s) ; 'fNL ;
 	   if !print_closed_sections then
              [< 'sTR " " ; hOV 0 [< print_context with_values ctxt >] >]
 	   else 
 	     [< >] >]
-    | (sp,Lib.OpenDir(str,_)) -> 
+    | (_,Lib.OpenedSection str) -> 
         [< 'sTR(" >>>>>>> Section " ^ str) ; 'fNL >]
-    | (_,Lib.Import(s,_,true)) ->
-	[< 'sTR" >>>>>>> Import " ; 'sTR s ; 'fNL >]
-    | (_,Lib.Import(s,_,false)) ->
-	[< 'sTR" >>>>>>> Export " ; 'sTR s ; 'fNL >]
-
+    | (_,Lib.FrozenState _) ->
+	[< >]
+	
 and print_context with_values = 
   let rec prec = function
     | h::rest -> [< prec rest ; print_library_entry with_values h >]
@@ -306,7 +308,7 @@ let print_full_context_typ () = print_context false (Lib.contents_after None)
 
 let rec head_const c = match strip_outer_cast c with
   | DOP2(Prod,_,DLAM(_,c)) -> head_const c
-  | DOPN(AppL,cl)    -> head_const (hd_vect cl)
+  | DOPN(AppL,cl)    -> head_const (array_hd cl)
   | def         -> def
 
 let list_filter_vec f vec = 
@@ -328,63 +330,57 @@ let list_filter_vec f vec =
 
 let print_constructors_head 
   (fn:string -> unit assumptions -> constr -> unit) c mip = 
-  let (lna,lC) = decomp_all_DLAMV_name mip.mINDLC in
+  let (lna,lC) = decomp_all_DLAMV_name mip.mind_lc in
   let ass_name = assumptions_for_print lna in
-  let lidC = map2_vect (fun id c_0 -> (id,c_0)) mip.mINDCONSNAMES lC in
+  let lidC = array_map2 (fun id c_0 -> (id,c_0)) mip.mind_consnames lC in
   let flid = list_filter_vec (fun (_,c_0) -> head_const c_0 = c) lidC in
   List.iter
     (function (id,c_0) -> fn (string_of_id id) ass_name c_0) flid
     
 let print_all_constructors_head fn c mib = 
-  let mipvec = mib.mINDPACKETS 
-  and n = mib.mINDNTYPES in 
-  let rec prec i = 
-    if i = n then 
-      mSG([< >])
-    else begin
-      print_constructors_head fn c mipvec.(i); 
-      prec (i+1)
-    end
-  in 
-  prec 0 
+  let mipvec = mib.mind_packets 
+  and n = mib.mind_ntypes in 
+  for i = 0 to n-1 do
+    print_constructors_head fn c mipvec.(i)
+  done
 
 let print_constructors_rel fn mip = 
-  let (lna,lC) = decomp_all_DLAMV_name mip.mINDLC in
+  let (lna,lC) = decomp_all_DLAMV_name mip.mind_lc in
   let ass_name = assumptions_for_print lna in
-  let lidC = map2_vect (fun id c -> (id,c)) mip.mINDCONSNAMES lC in
+  let lidC = array_map2 (fun id c -> (id,c)) mip.mind_consnames lC in
   let flid = list_filter_vec (fun (_,c) -> isRel (head_const c)) lidC in
   List.iter (function (id,c) -> fn (string_of_id id) ass_name c) flid
 
 let crible (fn:string -> unit assumptions -> constr -> unit) name =
-  let imported = Library.search_imports() in
-  let const = Machops.global (gLOB(initial_sign())) name in 
+  let hyps = gLOB (get_globals (Global.context())) in
+  let imported = Library.opened_modules() in
+  let const = global_reference CCI name in 
   let rec crible_rec = function
-    | (spopt,Lib.LEAF lobj)::rest ->
+    | (spopt,Lib.Leaf lobj)::rest ->
 	(match (spopt,object_tag lobj) with
 	   | (_,"VARIABLE") ->
-	       let (namec,(typ,_),_,_,_,_) = outVariable lobj in 
-               (if (head_const typ.body)=const then  
-                  fn (string_of_id namec) (gLOB(initial_sign())) typ.body);
+	       let (namec,typ,_) = out_variable spopt in 
+               if (head_const typ.body) = const then  
+                 fn (string_of_id namec) hyps typ.body;
                crible_rec rest
 	   | (sp,"CONSTANT") ->
-	       let (_,{cONSTTYPE=typ}) = const_of_path (ccisp_of sp) in
-               (if (head_const typ.body)=const then
-                  fn (print_basename sp) (gLOB(initial_sign())) typ.body);
+	       let {const_type=typ} = Global.lookup_constant sp in
+               if (head_const typ.body) = const then
+                 fn (print_basename sp) hyps typ.body;
                crible_rec rest
 	   | (sp,"MUTUALINDUCTIVE") -> 
-               let (_,mib) = mind_of_path (ccisp_of sp) in 
-               (match const with (DOPN(MutInd(sp',tyi),_)) 
-                    -> if sp = objsp_of sp' then print_constructors_rel fn
-                      (mind_nth_type_packet mib tyi) 
+               let mib = Global.lookup_mind sp in 
+               (match const with 
+		  | (DOPN(MutInd(sp',tyi),_)) -> 
+		      if sp = objsp_of sp' then print_constructors_rel fn
+			(mind_nth_type_packet mib tyi) 
 		  | _ -> print_all_constructors_head fn const mib); 
                crible_rec rest
 	   | _ -> crible_rec rest)
 
-    | (spopt,Lib.OpenDir _)::rest -> crible_rec rest
-    | (spopt,Lib.ClosedDir (_,_,_,libseg))::rest -> 
-        (if List.mem spopt imported then crible_rec libseg);
-        crible_rec rest
-    | (spopt,Lib.Import _)::rest -> crible_rec rest
+    | (_, (Lib.OpenedSection _ | Lib.ClosedSection _ 
+	  | Lib.FrozenState _))::rest -> 
+	crible_rec rest
     | []      -> ()
   in 
   try 
@@ -399,7 +395,7 @@ let print_crible name =
 
 let read_sec_context sec =
   let rec get_cxt in_cxt = function
-    | ((sp,Lib.OpenDir(str,_)) as hd)::rest ->
+    | ((sp,Lib.OpenedSection str) as hd)::rest ->
         if str = sec then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
     | [] -> []
     | hd::rest -> get_cxt (hd::in_cxt) rest 
@@ -411,16 +407,16 @@ let print_sec_context sec = print_context true (read_sec_context sec)
 
 let print_sec_context_typ sec = print_context false (read_sec_context sec)
 
-let print_val sign {_VAL=trm;_TYPE=typ} =
-  print_typed_value_in_sign sign (trm,typ)
+let print_val env {uj_val=trm;uj_type=typ} =
+  print_typed_value_in_env env (trm,typ)
     
-let print_type sign {_VAL=trm;_TYPE=typ} =
-  print_typed_value_in_sign sign (trm, nf_betaiota typ)
+let print_type env {uj_val=trm;uj_type=typ} =
+  print_typed_value_in_env env (trm, nf_betaiota env Evd.empty typ)
     
-let print_eval red_fun sign {_VAL=trm;_TYPE=typ} =
-  let ntrm = red_fun trm
-  and ntyp = nf_betaiota typ in
-  [< 'sTR "     = "; print_typed_value_in_sign sign (ntrm, ntyp) >]
+let print_eval red_fun env {uj_val=trm;uj_type=typ} =
+  let ntrm = red_fun env Evd.empty trm
+  and ntyp = nf_betaiota env Evd.empty typ in
+  [< 'sTR "     = "; print_typed_value_in_env env (ntrm, ntyp) >]
 
 let print_name name = 
   let str = string_of_id name in 
@@ -431,31 +427,32 @@ let print_name name =
   with 
     | Not_found -> 
 	(try 
-	   let typ = snd(lookup_glob name (gLOB (initial_sign ()))) in 
+	   let (_,typ) = Global.lookup_var name in 
 	   ([< print_var str typ;
-               try print_impl_args (Vartab.implicits_of_var CCI name)
+               try print_impl_args (implicits_of_var CCI name)
                with _ -> [<>] >]) 
 	 with Not_found | Invalid_argument _ -> 
 	   error (str ^ " not a defined object"))
     | Invalid_argument _ -> error (str ^ " not a defined object")
 
 let print_opaque_name name = 
-  let (sigma,sign) = initial_sigma_sign() in
+  let sigma = Evd.empty in
+  let env = Global.unsafe_env () in
+  let sign = get_globals (Global.context ()) in
   try 
-    match (Machops.global (gLOB sign) name) with
+    match global_reference CCI name with
       | DOPN(Const sp,_) as x ->
-          if evaluable_const sigma x then
-            print_typed_value(const_value sigma x,const_type sigma x)
-          else begin
-            Constants.set_transparent_sp sp;
-            let valu = const_value sigma x in 
-	    Constants.set_opaque_sp sp;
-            print_typed_value(valu,const_type sigma x)
-	  end
+	  let cb = Global.lookup_constant sp in
+          if is_defined cb then
+	    let typ = constant_type env x in
+            print_typed_value (constant_value env x,typ.body)
+          else 
+	    anomaly "print_opaque_name"
       | DOPN(MutInd (sp,_),_) as x ->
-          print_mutual CCI (snd (mind_of_path sp))
+          print_mutual sp (Global.lookup_mind sp)
       | DOPN(MutConstruct _,_) as x -> 
-          print_typed_value(x, type_of sigma sign x)
+	  let ty = Typeops.type_of_constructor env sigma x in
+	  print_typed_value(x, ty)
       | VAR id ->
           let a = snd(lookup_sign id sign) in 
 	  print_var (string_of_id id) a
@@ -467,9 +464,9 @@ let print_local_context () =
   let env = Lib.contents_after None in
   let rec print_var_rec = function 
     | [] -> [< >]
-    | ((_,Lib.LEAF lobj))::rest ->
+    | (sp,Lib.Leaf lobj)::rest ->
 	if "VARIABLE" = object_tag lobj then
-          let (name,(typ,_),_,_,_,_) = outVariable lobj in 
+          let (name,typ,_) = out_variable sp in 
 	  [< print_var_rec rest;
              print_var (string_of_id name) typ >]
 	else 
@@ -477,20 +474,20 @@ let print_local_context () =
     | _::rest -> print_var_rec rest
 
   and print_last_const = function
-    | (sp,Lib.LEAF lobj)::rest -> 
+    | (sp,Lib.Leaf lobj)::rest -> 
         (match object_tag lobj with
            | "CONSTANT" -> 
-               let (_,{cONSTBODY=val_0;cONSTTYPE=typ}) = 
-		 const_of_path (ccisp_of sp) in
+               let {const_body=val_0;const_type=typ} = 
+		 Global.lookup_constant sp in
                [< print_last_const rest;
                   'sTR(print_basename sp) ;'sTR" = ";
                   print_typed_recipe (val_0,typ) >]
            | "MUTUALINDUCTIVE" -> 
-               let (_,mib) = mind_of_path (ccisp_of sp) in 
-               [< print_last_const rest;print_mutual CCI mib; 'fNL >]
+               let mib = Global.lookup_mind sp in 
+               [< print_last_const rest;print_mutual sp mib; 'fNL >]
            |  "VARIABLE" ->  [< >]
            |  _          ->  print_last_const rest)
-    | (sp,Lib.ClosedDir _)::rest -> print_last_const rest
+    | (sp,Lib.ClosedSection _)::rest -> print_last_const rest
     | _ -> [< >]
   in 
   [< print_var_rec env;  print_last_const env >]
@@ -498,18 +495,19 @@ let print_local_context () =
 let fprint_var name typ =
   [< 'sTR ("*** [" ^ name ^ " :"); fprtype typ; 'sTR "]"; 'fNL >]
 
-let fprint_judge {_VAL=trm;_TYPE=typ} = 
+let fprint_judge {uj_val=trm;uj_type=typ} = 
   [< fprterm trm; 'sTR" : " ; fprterm typ >]
 
-let unfold_head_fconst sigma = 
+let unfold_head_fconst = 
   let rec unfrec = function
-    | DOPN(Const _,_) as k -> const_value sigma k 
+    | DOPN(Const _,_) as k -> constant_value (Global.unsafe_env()) k 
     | DOP2(Lambda,t,DLAM(na,b)) -> DOP2(Lambda,t,DLAM(na,unfrec b))
-    | DOPN(AppL,v) -> DOPN(AppL,cons_vect (unfrec (hd_vect v)) (tl_vect v))
+    | DOPN(AppL,v) -> DOPN(AppL,array_cons (unfrec (array_hd v)) (array_tl v))
     | x -> x
   in 
   unfrec
 
+(***
 let print_extracted_name name =
   let (sigma,(sign,fsign)) = initial_sigma_assumptions() in
   try
@@ -651,6 +649,7 @@ let print_extracted_vars () =
     | [] -> [< 'fNL >]
   in 
   print_var_rec env
+***)
 
 (* for debug *)
 let inspect depth = 
diff --git a/parsing/pretty.mli b/parsing/pretty.mli
index 2b4c378c2d..dd8d605ed4 100644
--- a/parsing/pretty.mli
+++ b/parsing/pretty.mli
@@ -27,18 +27,23 @@ val print_full_context_typ : unit -> std_ppcmds
 val print_crible : identifier -> unit
 val print_sec_context : string -> std_ppcmds
 val print_sec_context_typ : string -> std_ppcmds
-val print_val : context -> unsafe_judgment -> std_ppcmds
-val print_type : context -> unsafe_judgment -> std_ppcmds
+val print_val : unsafe_env -> unsafe_judgment -> std_ppcmds
+val print_type : unsafe_env -> unsafe_judgment -> std_ppcmds
 val print_eval :
-  'a reduction_function -> context -> unsafe_judgment -> std_ppcmds
-val implicit_args_msg : mutual_inductive_packet array -> std_ppcmds
-val print_mutual : path_kind -> mutual_inductive_body -> std_ppcmds
+  'a reduction_function -> unsafe_env -> unsafe_judgment -> std_ppcmds
+val implicit_args_msg : 
+  section_path -> mutual_inductive_packet array -> std_ppcmds
+val print_mutual : section_path -> mutual_inductive_body -> std_ppcmds
 val print_name : identifier -> std_ppcmds
 val print_opaque_name : identifier -> std_ppcmds
 val print_local_context : unit -> std_ppcmds
+
+(*i
 val print_extracted_name : identifier -> std_ppcmds
 val print_extraction : unit -> std_ppcmds
 val print_extracted_vars : unit -> std_ppcmds
+i*)
+
 val crible : (string -> unit assumptions -> constr -> unit) -> identifier ->
   unit
 val inspect : int -> std_ppcmds
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index f69253eea8..533d1f3c1b 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -148,7 +148,10 @@ let (inClass,outClass) =
                     specification_function = (function x -> x) })
 
 let add_new_class (cl,s,stre,p) = 
-  Lib.add_anonymous_leaf (inClass ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p})))
+  let _ = 
+    Lib.add_anonymous_leaf (inClass ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p})))
+  in
+  ()
     
 let _ = 
   Summary.declare_summary "inh_graph"
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 0ee1e04349..f2df08842d 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -29,7 +29,7 @@ type reference =
   | RConstruct of constructor_id * identifier list
   | RAbst of section_path
   | RVar of identifier
-  | REVar of section_path * identifier list
+  | REVar of int * identifier list
   | RMeta of int
 
 type cases_style = PrintLet | PrintIf | PrintCases
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index dea95d0e04..590eff02b2 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -44,7 +44,9 @@ let (inStruc,outStruc) =
                     specification_function = (function x -> x) })
 
 let add_new_struc (s,c,n,l) = 
-  Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l}))
+  let _ = 
+    Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l})) in
+  ()
 
 let struc_info s = List.assoc s !sTRUCS
 
@@ -81,8 +83,9 @@ let add_new_objdef (o,c,la,lp,l) =
   try 
     let _ = List.assoc o !oBJDEFS in ()
   with Not_found -> 
-    Lib.add_anonymous_leaf
-      (inObjDef (o,{o_DEF=c;o_TABS=la;o_TPARAMS=lp;o_TCOMPS=l}))
+    let _ = Lib.add_anonymous_leaf
+	      (inObjDef (o,{o_DEF=c;o_TABS=la;o_TPARAMS=lp;o_TCOMPS=l})) in
+    ()
 
 let ((inObjDef1:section_path -> obj),(outObjDef1:obj -> section_path)) =
   declare_object ("OBJDEF1",