Réforme de l'interprétation des termes :

- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
  pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
  se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
  constrextern.ml est l'équivalent de termast.ml pour le nouveau
  printer; topconstr.ml; contient la définition de "constr_expr";
  modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid


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

33 files changed, 306 insertions, 244 deletions

diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4
index f7a9e723fa..ca4a249685 100644
--- a/contrib/cc/cctac.ml4
+++ b/contrib/cc/cctac.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i camlp4deps: "parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo" i*)
+(*i camlp4deps: "parsing/grammar.cma" i*)
 
 (* $Id$ *)
 
@@ -33,7 +33,7 @@ exception Not_an_eq
 let fail()=raise Not_an_eq
     
 let constr_of_string s () =
-  Declare.constr_of_reference (Nametab.locate (qualid_of_string s))
+  constr_of_reference (Nametab.locate (qualid_of_string s))
 
 let eq2eqT_theo = constr_of_string "Coq.Logic.Eqdep_dec.eq2eqT"
 let eqT2eq_theo = constr_of_string "Coq.Logic.Eqdep_dec.eqT2eq"
@@ -58,7 +58,7 @@ let eq_type_of_term term=
   match kind_of_term term with
       App (f,args)->
 	(try 
-	   let ref = Declare.reference_of_constr f in
+	   let ref = reference_of_constr f in
 	     if (ref=Coqlib.glob_eq || ref=Coqlib.glob_eqT) && 
 	       (Array.length args)=3 
 	     then (args.(0),args.(1),args.(2)) 
diff --git a/contrib/correctness/past.mli b/contrib/correctness/past.mli
index 3c5a56c1df..b761da60ea 100644
--- a/contrib/correctness/past.mli
+++ b/contrib/correctness/past.mli
@@ -14,10 +14,11 @@
 
 open Names
 open Ptype
+open Topconstr
 
 type termination = 
   | RecArg of int 
-  | Wf of Coqast.t * Coqast.t
+  | Wf of constr_expr * constr_expr
 
 type variable = identifier
 
@@ -43,7 +44,7 @@ type ('a, 'b) t = {
   desc : ('a, 'b) t_desc;
   pre  : 'b Ptype.precondition list;
   post : 'b Ptype.postcondition option;
-  loc  : Coqast.loc;
+  loc  : Util.loc;
   info : 'a 
 }
 
@@ -73,7 +74,7 @@ and ('a, 'b) arg =
   | Refarg of variable
   | Type of 'b Ptype.ml_type_v
 
-type program = (unit, Coqast.t) t
+type program = (unit, Topconstr.constr_expr) t
 
 (*s Intermediate type for CC terms. *)
 
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index 30959acdad..488819bc24 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -10,7 +10,9 @@
 
 (* $Id$ *)
 
+open Util
 open Names
+open Nameops
 open Libnames
 open Term
 open Termops
@@ -21,6 +23,7 @@ open Sign
 open Rawterm
 open Typeops
 open Entries
+open Topconstr
 
 open Pmisc
 open Past
@@ -39,26 +42,21 @@ let tuple_exists id =
   try let _ = Nametab.locate (make_short_qualid id) in true
   with Not_found -> false
 
-let ast_set = Ast.ope ("SET", [])
+let ast_set = CSort (dummy_loc,RProp Pos)
 
 let tuple_n n =
-  let name = "tuple_" ^ string_of_int n in
-  let id = id_of_string name in
+  let id = make_ident "tuple_" (Some n) in
   let l1n = Util.interval 1 n in
-  let params = 
-    List.map 
-      (fun i -> let id = id_of_string ("T" ^ string_of_int i) in (id, ast_set))
-      l1n
-  in
+  let params = List.map (fun i -> (make_ident "T" (Some i), ast_set)) l1n in
   let fields = 
     List.map
       (fun i -> 
-	 let id = id_of_string 
-		    ("proj_" ^ string_of_int n ^ "_" ^ string_of_int i) in
-	 (false, Vernacexpr.AssumExpr (id, Ast.nvar (id_of_string ("T" ^ string_of_int i)))))
+	 let id = make_ident ("proj_" ^ string_of_int n ^ "_") (Some i) in
+	 let id' = make_ident "T" (Some i) in
+	 (false, Vernacexpr.AssumExpr (id, mkIdentC id')))
       l1n 
   in
-  let cons = id_of_string ("Build_tuple_" ^ string_of_int n) in
+  let cons = make_ident "Build_tuple_" (Some n) in
   Record.definition_structure ((false, id), params, fields, cons, mk_Set)
 
 (*s [(sig_n n)] generates the inductive
@@ -68,12 +66,11 @@ let tuple_n n =
     \end{verbatim} *)
 
 let sig_n n =
-  let name = "sig_" ^ string_of_int n in
-  let id = id_of_string name in
+  let id = make_ident "sig_" (Some n) in
   let l1n = Util.interval 1 n in
-  let lT = List.map (fun i -> id_of_string ("T" ^ string_of_int i)) l1n in
-  let lx = List.map (fun i -> id_of_string ("x" ^ string_of_int i)) l1n in
-  let idp = id_of_string "P" in
+  let lT = List.map (fun i -> make_ident "T" (Some i)) l1n in
+  let lx = List.map (fun i -> make_ident "x" (Some i)) l1n in
+  let idp = make_ident "P" None in
   let params =
     let typ = List.fold_right (fun _ c -> mkArrow (mkRel n) c) lT mkProp in
     (idp, LocalAssum typ) :: 
@@ -87,7 +84,7 @@ let sig_n n =
     let c = mkArrow app_p app_sig in
     List.fold_right (fun id c -> mkProd (Name id, mkRel (n+1), c)) lx c
   in
-  let cname = id_of_string ("exist_" ^ string_of_int n) in
+  let cname = make_ident "exist_" (Some n) in
   Declare.declare_mind 
     { mind_entry_finite = true;
       mind_entry_inds = 
@@ -123,14 +120,12 @@ let tuple_ref dep n =
       if n = 1 then 
 	exist
       else begin
-	let name = Printf.sprintf "exist_%d" n in
-	let id = id_of_string name in
+	let id = make_ident "exist_" (Some n) in
 	if not (tuple_exists id) then ignore (sig_n n);
 	Nametab.locate (make_short_qualid id)
       end
     else begin
-      let name = Printf.sprintf "Build_tuple_%d" n in
-      let id = id_of_string name in
+      let id = make_ident "Build_tuple_%d" (Some n) in
       if not (tuple_exists id) then tuple_n n;
       Nametab.locate (make_short_qualid id)
     end
@@ -185,7 +180,7 @@ let rawconstr_of_prog p =
 	let (bl',avoid',nenv') = push_vars avoid nenv bl in
 	let c1 = trad avoid nenv e1
 	and c2 = trad avoid' nenv' e2 in
-	ROldCase (dummy_loc, false, None, c1, [| raw_lambda bl' c2 |])
+	ROrderedCase (dummy_loc, LetStyle, None, c1, [| raw_lambda bl' c2 |])
 
     | CC_lam (bl,e) ->
 	let bl',avoid',nenv' = push_vars avoid nenv bl in
@@ -219,7 +214,7 @@ let rawconstr_of_prog p =
 	let c = trad avoid nenv b in
 	let cl = List.map (trad avoid nenv) el in
 	let ty = Detyping.detype (Global.env()) avoid nenv ty in
-	ROldCase (dummy_loc, false, Some ty, c, Array.of_list cl)
+	ROrderedCase (dummy_loc, RegularStyle, Some ty, c, Array.of_list cl)
 
     | CC_expr c -> 
 	Detyping.detype (Global.env()) avoid nenv c
diff --git a/contrib/correctness/perror.mli b/contrib/correctness/perror.mli
index 81bed4404c..3664ebf787 100644
--- a/contrib/correctness/perror.mli
+++ b/contrib/correctness/perror.mli
@@ -11,10 +11,10 @@
 (* $Id$ *)
 
 open Pp
+open Util
 open Names
 open Ptype
 open Past
-open Coqast
 
 val unbound_variable : identifier -> loc option -> 'a
 val unbound_reference : identifier -> loc option -> 'a
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index bb660ddb4c..60f7306ac5 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -12,10 +12,11 @@
 
 open Pp
 open Util
-open Coqast
 open Names
 open Nameops
 open Term
+open Libnames
+open Topconstr
 
 (* debug *)
 
@@ -122,6 +123,7 @@ let subst_in_constr alist =
   let alist' = List.map (fun (id,id') -> (id, mkVar id')) alist in
   replace_vars alist'
 
+(*
 let subst_in_ast alist ast =
   let rec subst = function
       Nvar(l,s) -> Nvar(l,try List.assoc s alist with Not_found -> s)
@@ -130,7 +132,8 @@ let subst_in_ast alist ast =
     | x -> x
   in
     subst ast
-
+*)
+(*
 let subst_ast_in_ast alist ast =
   let rec subst = function
       Nvar(l,s) as x -> (try List.assoc s alist with Not_found -> x)
@@ -139,6 +142,17 @@ let subst_ast_in_ast alist ast =
     | x -> x
   in
     subst ast
+*)
+
+let rec subst_in_ast alist = function
+  | CRef (Ident (loc,id)) ->
+      CRef (Ident (loc,(try List.assoc id alist with Not_found -> id)))
+  | x -> map_constr_expr_with_binders subst_in_ast List.remove_assoc alist x
+
+let rec subst_ast_in_ast alist = function
+  | CRef (Ident (_,id)) as x -> (try List.assoc id alist with Not_found -> x)
+  | x ->
+      map_constr_expr_with_binders subst_ast_in_ast List.remove_assoc alist x
 
 (* subst. of variables by constr *)
 let real_subst_in_constr = replace_vars
diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli
index 207e74b2be..a07eed5659 100644
--- a/contrib/correctness/pmisc.mli
+++ b/contrib/correctness/pmisc.mli
@@ -13,10 +13,11 @@
 open Names
 open Term
 open Ptype
+open Topconstr
 
 (* Some misc. functions *)
 
-val reraise_with_loc : Coqast.loc -> ('a -> 'b) -> 'a -> 'b
+val reraise_with_loc : Util.loc -> ('a -> 'b) -> 'a -> 'b
 
 val list_of_some : 'a option -> 'a list
 val difference : 'a list -> 'a list -> 'a list
@@ -49,8 +50,9 @@ val id_of_name : name -> identifier
 val isevar : constr
 
 val subst_in_constr : (identifier * identifier) list -> constr -> constr
-val subst_in_ast : (identifier * identifier) list -> Coqast.t -> Coqast.t
-val subst_ast_in_ast : (identifier * Coqast.t) list -> Coqast.t -> Coqast.t
+val subst_in_ast : (identifier * identifier) list -> constr_expr -> constr_expr
+val subst_ast_in_ast :
+  (identifier * constr_expr) list -> constr_expr -> constr_expr
 val real_subst_in_constr : (identifier * constr) list -> constr -> constr
 
 val constant : string -> constr
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 591076bddb..8e4c9b2bd3 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -13,11 +13,14 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Options
+open Util
 open Names
 open Nameops
 open Vernacentries
 open Reduction
 open Term
+open Libnames
+open Topconstr
 
 open Prename
 open Pmisc
@@ -92,17 +95,23 @@ module Programs =
 open Programs
 
 let ast_of_int n =
-  G_zsyntax.z_of_string true n Ast.dummy_loc
+  G_zsyntax.z_of_string true n dummy_loc
 
 let constr_of_int n =
-  Astterm.interp_constr Evd.empty (Global.env ()) (ast_of_int n)
+  Constrintern.interp_constr Evd.empty (Global.env ()) (ast_of_int n)
+
+open Util
+open Coqast
 
-let ast_constant loc s = <:ast< (QUALID ($VAR $s)) >>
+let mk_id loc id = mkRefC (Ident (loc, id))
+let mk_ref loc s = mk_id loc (id_of_string s)
+let mk_appl loc1 loc2 f args =
+  CApp (join_loc loc1 loc2, mk_ref loc1 f, List.map (fun a -> a,None) args)
 
 let conj_assert {a_name=n;a_value=a} {a_value=b} = 
-  let loc = Ast.loc a in
-  let et = ast_constant loc "and" in
-  { a_value = <:ast< (APPLIST $et $a $b) >>; a_name = n }
+  let loc1 = constr_loc a in
+  let loc2 = constr_loc a in
+  { a_value = mk_appl loc1 loc2 "and" [a;b]; a_name = n }
 
 let conj = function
     None,None     -> None
@@ -137,28 +146,26 @@ let bool_not loc a =
   let d = SApp ( [Variable connective_not ], [a]) in
   w d
 
-let ast_zwf_zero loc =
-  let zwf = ast_constant loc "Zwf" and zero = ast_constant loc "ZERO" in
-    <:ast< (APPLIST $zwf $zero) >>
+let ast_zwf_zero loc = mk_appl loc loc "Zwf" [mk_ref loc "ZERO"]
 
 (* program -> Coq AST *)
 
-let bdize c = 
+let bdize c =
   let env = 
     Global.env_of_context (Pcicenv.cci_sign_of Prename.empty_ren Penv.empty)
   in
-  Termast.ast_of_constr true env c
+  Constrextern.extern_constr true env c
 
 let rec coqast_of_program loc = function
-  | Variable id -> let s = string_of_id id in <:ast< ($VAR $s) >>
-  | Acc id -> let s = string_of_id id in <:ast< ($VAR $s) >>
+  | Variable id -> mk_id loc id
+  | Acc id -> mk_id loc id
   | Apply (f,l) -> 
       let f = coqast_of_program f.loc f.desc in
       let args = List.map 
-		   (function Term t -> coqast_of_program t.loc t.desc
+		   (function Term t -> (coqast_of_program t.loc t.desc,None)
 		      | _ -> invalid_arg "coqast_of_program") l
       in
-      <:ast< (APPLIST $f ($LIST $args)) >>
+      CApp (dummy_loc, f, args)
   | Expression c -> bdize c
   | _ -> invalid_arg "coqast_of_program"
 
@@ -174,9 +181,8 @@ let rec coqast_of_program loc = function
  *)
 
 let ast_plus_un loc ast =
-  let zplus = ast_constant loc "Zplus" in
   let un = ast_of_int "1" in
-  <:ast< (APPLIST $zplus $ast $un) >>
+  mk_appl loc loc "Zplus" [ast;un]
 
 let make_ast_for loc i v1 v2 inv block =
   let f = for_name() in
@@ -197,22 +203,20 @@ let make_ast_for loc i v1 v2 inv block =
       without_effect loc (Seq (block @ [Statement f_succ_i]))
     in
     let inv' = 
-      let zle = ast_constant loc "Zle" in
-      let i_le_sv2 = <:ast< (APPLIST $zle ($VAR $i) $succ_v2) >> in
+      let i_le_sv2 = mk_appl loc loc "Zle" [mk_ref loc i; succ_v2] in
       conj_assert {a_value=i_le_sv2;a_name=inv.a_name} inv
     in
     { desc = If(test,br_t,br_f); loc = loc; 
       pre = [pre_of_assert false inv']; post = Some post; info = () } 
   in
   let bl = 
-    let typez = ast_constant loc "Z" in
+    let typez = mk_ref loc "Z" in
     [(id_of_string i, BindType (TypePure typez))] 
   in
   let fv1 = without_effect loc (Apply (var_f, [Term v1])) in
-  let v = TypePure (ast_constant loc "unit") in
+  let v = TypePure (mk_ref loc "unit") in
   let var = 
-    let zminus = ast_constant loc "Zminus" in
-    let a = <:ast< (APPLIST $zminus $succ_v2 ($VAR $i)) >> in
+    let a = mk_appl loc loc "Zminus" [succ_v2;mk_ref loc i] in
     (a, ast_zwf_zero loc)
   in
   Let (f, without_effect loc (LetRec (f,bl,v,var,e1)), fv1)
diff --git a/contrib/correctness/psyntax.mli b/contrib/correctness/psyntax.mli
index f5128fdef9..dac571de55 100644
--- a/contrib/correctness/psyntax.mli
+++ b/contrib/correctness/psyntax.mli
@@ -13,13 +13,14 @@
 open Pcoq
 open Ptype
 open Past
+open Topconstr
 
 (* Grammar for the programs and the tactic Correctness *)
 
 module Programs :
   sig
     val program : program Gram.Entry.e
-    val type_v  : Coqast.t ml_type_v Gram.Entry.e
-    val type_c  : Coqast.t ml_type_c Gram.Entry.e
+    val type_v  : constr_expr ml_type_v Gram.Entry.e
+    val type_c  : constr_expr ml_type_c Gram.Entry.e
   end
 
diff --git a/contrib/correctness/ptyping.ml b/contrib/correctness/ptyping.ml
index a6f7a0ae95..6c870c85a8 100644
--- a/contrib/correctness/ptyping.ml
+++ b/contrib/correctness/ptyping.ml
@@ -16,9 +16,10 @@ open Names
 open Term
 open Termops
 open Environ
-open Astterm
+open Constrintern
 open Himsg
 open Proof_trees
+open Topconstr
 
 open Pmisc
 open Putil
@@ -110,7 +111,7 @@ let effect_app ren env f args =
 let state_coq_ast sign a =
   let env = Global.env_of_context sign in
   let j =
-    reraise_with_loc (Ast.loc a) (judgment_of_rawconstr Evd.empty env) a in
+    reraise_with_loc (constr_loc a) (judgment_of_rawconstr Evd.empty env) a in
   let ids = global_vars env j.uj_val in
   j.uj_val, j.uj_type, ids
 
diff --git a/contrib/correctness/ptyping.mli b/contrib/correctness/ptyping.mli
index bfb7a9a869..968f4fd31e 100644
--- a/contrib/correctness/ptyping.mli
+++ b/contrib/correctness/ptyping.mli
@@ -12,6 +12,7 @@
 
 open Names
 open Term
+open Topconstr
 
 open Ptype
 open Past
@@ -19,7 +20,7 @@ open Penv
 
 (* This module realizes type and effect inference *)
 
-val cic_type_v : local_env -> Prename.t -> Coqast.t ml_type_v -> type_v
+val cic_type_v : local_env -> Prename.t -> constr_expr ml_type_v -> type_v
 
 val effect_app : Prename.t -> local_env
             -> (typing_info,'b) Past.t
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli
index 2151618982..a49b3b4ff8 100644
--- a/contrib/extraction/extract_env.mli
+++ b/contrib/extraction/extract_env.mli
@@ -14,8 +14,8 @@ open Util
 open Names
 open Libnames
 
-val extraction : qualid located -> unit
-val extraction_rec : qualid located list -> unit
-val extraction_file : string -> qualid located list -> unit
+val extraction : reference -> unit
+val extraction_rec : reference list -> unit
+val extraction_file : string -> reference list -> unit
 val extraction_module : identifier -> unit
 val recursive_extraction_module : identifier -> unit
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index 1ae18f77e6..46021af732 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -34,11 +34,11 @@ END
 
 VERNAC COMMAND EXTEND Extraction
 (* Extraction in the Coq toplevel *)
-| [ "Extraction" qualid(x) ] -> [ extraction x ]
-| [ "Recursive" "Extraction" ne_qualid_list(l) ] -> [ extraction_rec l ]
+| [ "Extraction" global(x) ] -> [ extraction x ]
+| [ "Recursive" "Extraction" ne_global_list(l) ] -> [ extraction_rec l ]
 
 (* Monolithic extraction to a file *)
-| [ "Extraction" string(f) ne_qualid_list(l) ] 
+| [ "Extraction" string(f) ne_global_list(l) ] 
   -> [ extraction_file f l ]
 END
 
@@ -61,12 +61,12 @@ END
 
 VERNAC COMMAND EXTEND ExtractionInline
 (* Custom inlining directives *)
-| [ "Extraction" "Inline" ne_qualid_list(l) ] 
+| [ "Extraction" "Inline" ne_global_list(l) ] 
   -> [ extraction_inline true l ]
 END
 
 VERNAC COMMAND EXTEND ExtractionNoInline
-| [ "Extraction" "NoInline" ne_qualid_list(l) ] 
+| [ "Extraction" "NoInline" ne_global_list(l) ] 
   -> [ extraction_inline false l ]
 END
 
@@ -82,16 +82,16 @@ END
 
 (* Overriding of a Coq object by an ML one *)
 VERNAC COMMAND EXTEND ExtractionConstant
-| [ "Extract" "Constant" qualid(x) "=>" mlname(y) ]
+| [ "Extract" "Constant" global(x) "=>" mlname(y) ]
   -> [ extract_constant_inline false x y ]
 END
 
 VERNAC COMMAND EXTEND ExtractionInlinedConstant
-| [ "Extract" "Inlined" "Constant" qualid(x) "=>" mlname(y) ]
+| [ "Extract" "Inlined" "Constant" global(x) "=>" mlname(y) ]
   -> [ extract_constant_inline true x y ]
 END
 
 VERNAC COMMAND EXTEND ExtractionInductive
-| [ "Extract" "Inductive" qualid(x) "=>" mlname(id) "[" mlname_list(idl) "]" ]
+| [ "Extract" "Inductive" global(x) "=>" mlname(id) "[" mlname_list(idl) "]" ]
   -> [ extract_inductive x (id,idl) ]
 END
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 7931dba01e..c951116ba0 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -57,14 +57,14 @@ open Util
 
 val extraction_language : lang -> unit
 
-val extraction_inline : bool -> qualid located list -> unit
+val extraction_inline : bool -> reference list -> unit
 
 val print_extraction_inline : unit -> unit
 
 val reset_extraction_inline : unit -> unit
 
-val extract_constant_inline : bool -> qualid located -> string -> unit
+val extract_constant_inline : bool -> reference -> string -> unit
 
-val extract_inductive : qualid located -> string * string list -> unit
+val extract_inductive : reference -> string * string list -> unit
 
 
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index d5c50f9d34..12be9a651e 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i camlp4deps: "parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo  parsing/g_ltac.cmo parsing/g_constr.cmo" i*)
+(*i camlp4deps: "parsing/grammar.cma" i*)
 
 (* $Id$ *)
 
@@ -23,7 +23,7 @@ open Vernacexpr
 open Tacexpr
 
 (* Interpretation of constr's *)
-let constr_of com = Astterm.interp_constr Evd.empty (Global.env()) com
+let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
 
 (* Construction of constants *)
 let constant dir s =
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index aac632de98..1398499cf5 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -73,9 +73,9 @@ let flin_emult a f =
 (*****************************************************************************)
 open Vernacexpr
 let parse_ast   = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse s = Astterm.interp_constr Evd.empty (Global.env()) (parse_ast s);;
+let parse s = Constrintern.interp_constr Evd.empty (Global.env()) (parse_ast s);;
 let pf_parse_constr gl s =
-   Astterm.interp_constr Evd.empty (pf_env gl) (parse_ast s);;
+   Constrintern.interp_constr Evd.empty (pf_env gl) (parse_ast s);;
 
 let string_of_R_constant kn = 
   match Names.repr_kn kn with
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 4c57760de0..d5715fd3d5 100755
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -4,7 +4,6 @@
 open Ctast;;
 open Termops;;
 open Nameops;;
-open Astterm;;
 open Auto;;
 open Clenv;;
 open Command;;
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index b917f24d4b..3a4806924b 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -40,7 +40,7 @@ open Blast;;
 open Dad;;
 open Debug_tac;;
 open Search;;
-open Astterm;;
+open Constrintern;;
 open Nametab;;
 open Showproof;;
 open Showproof_ct;;
@@ -494,9 +494,9 @@ let pcoq_reset_initial() =
 let pcoq_reset x =
   if refining() then
     output_results (ctf_AbortedAllMessage ()) None;
-    Vernacentries.abort_refine Lib.reset_name x;
+    Vernacentries.abort_refine Lib.reset_name (dummy_loc,x);
     output_results
-         (ctf_ResetIdentMessage !global_request_id (string_of_id x)) None;;
+      (ctf_ResetIdentMessage !global_request_id (string_of_id x)) None;;
 
 
 VERNAC ARGUMENT EXTEND text_mode
@@ -568,8 +568,8 @@ let pcoq_search s l =
   end;
   search_output_results()
 
-let pcoq_print_name (_,qid) =
-  let results = xlate_vernac_list (name_to_ast qid) in
+let pcoq_print_name ref =
+  let results = xlate_vernac_list (name_to_ast ref) in
   output_results 
     (fnl () ++ str "message" ++ fnl () ++ str "PRINT_VALUE" ++ fnl ())
     (Some (P_cl results))
diff --git a/contrib/interface/ctast.ml b/contrib/interface/ctast.ml
index 2345ff4719..17bd6ef4e1 100644
--- a/contrib/interface/ctast.ml
+++ b/contrib/interface/ctast.ml
@@ -44,7 +44,8 @@ let rec ct_to_ast = function
   | Path (loc,sl) -> Coqast.Path (loc,section_path sl)
   | Dynamic (loc,a) -> Coqast.Dynamic (loc,a)
 
-let rec ast_to_ct = function
+let rec ast_to_ct = function x -> failwith "ast_to_ct: not TODO?"
+(*
   | Coqast.Node (loc,a,b) -> Node (loc,a,List.map ast_to_ct b)
   | Coqast.Nvar (loc,a) -> Nvar (loc,string_of_id a)
   | Coqast.Nmeta (loc,a) -> Nvar (loc,"$"^a)
@@ -60,6 +61,7 @@ let rec ast_to_ct = function
     Path(loc, (List.map string_of_id
                 (List.rev (repr_dirpath sl))) @ [string_of_id bn])
   | Coqast.Dynamic (loc,a) -> Dynamic (loc,a)
+*)
 
 let loc = function
   | Node (loc,_,_) -> loc
@@ -71,4 +73,4 @@ let loc = function
   | Path (loc,_) -> loc
   | Dynamic (loc,_) -> loc
 
-let str s = Str(Ast.dummy_loc,s)
+let str s = Str(Util.dummy_loc,s)
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index 3be5d8a36a..00a4bb07ec 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -12,8 +12,8 @@ open Tacticals;;
 open Pattern;;
 open Reduction;;
 open Ctast;;
-open Termast;;
-open Astterm;;
+open Constrextern;;
+open Constrintern;;
 open Vernacinterp;;
 open Libnames;;
 open Nametab
@@ -26,6 +26,7 @@ open Pp;;
 
 open Paths;;
 
+open Topconstr;;
 open Genarg;;
 open Tacexpr;;
 open Rawterm;;
@@ -43,7 +44,8 @@ open Rawterm;;
 
 
 type dad_rule =
-    Ctast.t * int list * int list * int * int list * raw_atomic_tactic_expr;;
+    constr_expr * int list * int list * int * int list
+    * raw_atomic_tactic_expr;;
 
 (* This value will be used systematically when constructing objects of
    type Ctast.t, the value is stupid and meaningless, but it is needed
@@ -68,6 +70,7 @@ let rec get_subterm  (depth:int) (path: int list) (constr:constr) =
    first argument, an object of type env, is necessary to
    transform constr terms into abstract syntax trees.  The second argument is
    the substitution, a list of pairs linking an integer and a constr term. *)
+(*
 let map_subst (env :env) 
    (subst:(int * Term.constr) list) =
    let rec map_subst_aux = function
@@ -77,13 +80,19 @@ let map_subst (env :env)
   | Coqast.Node(loc, s, l) -> Coqast.Node(loc, s, List.map map_subst_aux l)
   | ast -> ast in
     map_subst_aux;;
+*)
+let rec map_subst (env :env) (subst:(int * Term.constr) list) = function
+  | CMeta (_,i) ->
+      let constr = List.assoc i subst in
+      extern_constr false env constr
+  | x -> map_constr_expr_with_binders (map_subst env) (fun _ x -> x) subst x;;
 
 let map_subst_tactic env subst = function
-  | TacExtend ("Rewrite" as x,[b;cbl]) ->
+  | TacExtend (loc,("Rewrite" as x),[b;cbl]) ->
       let c,bl = out_gen rawwit_constr_with_bindings cbl in
       assert (bl = NoBindings);
       let c = (map_subst env subst c,NoBindings) in
-      TacExtend (x,[b;in_gen rawwit_constr_with_bindings c])
+      TacExtend (loc,x,[b;in_gen rawwit_constr_with_bindings c])
   | _ -> failwith "map_subst_tactic: unsupported tactic"
 
 (* This function is really the one that is important. *)
@@ -103,7 +112,7 @@ let rec find_cmd (l:(string * dad_rule) list) env constr p p1 p2 =
                 Failure s -> failwith "internal" in
          let _, constr_pat = 
             interp_constrpattern Evd.empty (Global.env())
-               (ct_to_ast pat) in
+               ((*ct_to_ast*) pat) in
          let subst = matches constr_pat term_to_match in
          if (is_prefix p_f (p_r@p1)) & (is_prefix p_l (p_r@p2)) then
            TacAtom (zz, map_subst_tactic env subst cmd)
@@ -251,11 +260,11 @@ let rec sort_list = function
     [] -> [] 
   | a::l -> add_in_list_sorting a (sort_list l);;
 
-let mk_dad_meta n = Node(zz,"META",[Num(zz, n)]);;
+let mk_dad_meta n = CMeta (zz,n);;
 let mk_rewrite lr ast =
   let b = in_gen rawwit_bool lr in
-  let cb = in_gen rawwit_constr_with_bindings (Ctast.ct_to_ast ast,NoBindings) in
-  TacExtend ("Rewrite",[b;cb])
+  let cb = in_gen rawwit_constr_with_bindings ((*Ctast.ct_to_ast*) ast,NoBindings) in
+  TacExtend (zz,"Rewrite",[b;cb])
 
 open Vernacexpr
 
@@ -279,101 +288,104 @@ END
 
 *)
 
+let mk_id s = mkIdentC (id_of_string s);;
+let mkMetaC = mk_dad_meta;;
+
 add_dad_rule "distributivity-inv"
-(Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,3)])]);Node(zz,"META",[Num(zz,2)])]))
+(mkAppC(mk_id("mult"),[mkAppC(mk_id("plus"),[mkMetaC(4);mkMetaC(3)]);mkMetaC(2)]))
 [2; 2]
 [2; 1]
 1
 [2]
-(mk_rewrite true (Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
+(mk_rewrite true (mkAppC(mk_id( "mult_plus_distr"),[(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
 
 add_dad_rule "distributivity1-r"
-(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,2)])]);Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])]))
+(mkAppC(mk_id("plus"),[mkAppC(mk_id("mult"),[mkMetaC(4);mkMetaC(2)]);mkAppC(mk_id("mult"),[mkMetaC(3);mkMetaC(2)])]))
 [2; 2; 2; 2]
 []
 0
 []
-(mk_rewrite false (Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
+(mk_rewrite false (mkAppC(mk_id("mult_plus_distr"),[(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
 
 add_dad_rule "distributivity1-l"
-(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,2)])]);Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])]))
+(mkAppC(mk_id("plus"),[mkAppC(mk_id("mult"),[mkMetaC(4);mkMetaC(2)]);mkAppC(mk_id("mult"),[mkMetaC(3);mkMetaC(2)])]))
 [2; 1; 2; 2]
 []
 0
 []
-(mk_rewrite false (Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
+(mk_rewrite false (mkAppC(mk_id( "mult_plus_distr"),[(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
 
 add_dad_rule "associativity"
-(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,3)])]);Node(zz,"META",[Num(zz,2)])]))
+(mkAppC(mk_id("plus"),[mkAppC(mk_id("plus"),[mkMetaC(4);mkMetaC(3)]);mkMetaC(2)]))
 [2; 1]
 []
 0
 []
-(mk_rewrite true (Node(zz, "APPLIST", [Nvar(zz, "plus_assoc_r");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
+(mk_rewrite true (mkAppC(mk_id( "plus_assoc_r"),[(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
 
 add_dad_rule "minus-identity-lr"
-(Node(zz,"APPLIST",[Nvar(zz,"minus");Node(zz,"META",[Num(zz,2)]);Node(zz,"META",[Num(zz,2)])]))
+(mkAppC(mk_id("minus"),[mkMetaC(2);mkMetaC(2)]))
 [2; 1]
 [2; 2]
 1
 [2]
-(mk_rewrite false (Node(zz, "APPLIST", [Nvar(zz, "minus_n_n");(mk_dad_meta 2) ])));
+(mk_rewrite false (mkAppC(mk_id( "minus_n_n"),[(mk_dad_meta 2) ])));
 
 add_dad_rule "minus-identity-rl"
-(Node(zz,"APPLIST",[Nvar(zz,"minus");Node(zz,"META",[Num(zz,2)]);Node(zz,"META",[Num(zz,2)])]))
+(mkAppC(mk_id("minus"),[mkMetaC(2);mkMetaC(2)]))
 [2; 2]
 [2; 1]
 1
 [2]
-(mk_rewrite false (Node(zz, "APPLIST", [Nvar(zz, "minus_n_n");(mk_dad_meta 2) ])));
+(mk_rewrite false (mkAppC(mk_id( "minus_n_n"),[(mk_dad_meta 2) ])));
 
 add_dad_rule "plus-sym-rl"
-(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])]))
+(mkAppC(mk_id("plus"),[mkMetaC(3);mkMetaC(2)]))
 [2; 2]
 [2; 1]
 1
 [2]
-(mk_rewrite true (Node(zz, "APPLIST", [Nvar(zz, "plus_sym");(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
+(mk_rewrite true (mkAppC(mk_id( "plus_sym"),[(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
 
 add_dad_rule "plus-sym-lr"
-(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])]))
+(mkAppC(mk_id("plus"),[mkMetaC(3);mkMetaC(2)]))
 [2; 1]
 [2; 2]
 1
 [2]
-(mk_rewrite true (Node(zz, "APPLIST", [Nvar(zz, "plus_sym");(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
+(mk_rewrite true (mkAppC(mk_id( "plus_sym"),[(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
 
 add_dad_rule "absorb-0-r-rl"
-(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,2)]);Nvar(zz,"O")]))
+(mkAppC(mk_id("plus"),[mkMetaC(2);mk_id("O")]))
 [2; 2]
 [1]
 0
 []
-(mk_rewrite false (Node(zz, "APPLIST", [Nvar(zz, "plus_n_O");(mk_dad_meta 2) ])));
+(mk_rewrite false (mkAppC(mk_id( "plus_n_O"),[(mk_dad_meta 2) ])));
 
 add_dad_rule "absorb-0-r-lr"
-(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,2)]);Nvar(zz,"O")]))
+(mkAppC(mk_id("plus"),[mkMetaC(2);mk_id("O")]))
 [1]
 [2; 2]
 0
 []
-(mk_rewrite false (Node(zz, "APPLIST", [Nvar(zz, "plus_n_O");(mk_dad_meta 2) ])));
+(mk_rewrite false (mkAppC(mk_id( "plus_n_O"),[(mk_dad_meta 2) ])));
 
 add_dad_rule "plus-permute-lr"
-(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])]))
+(mkAppC(mk_id("plus"),[mkMetaC(4);mkAppC(mk_id("plus"),[mkMetaC(3);mkMetaC(2)])]))
 [2; 1]
 [2; 2; 2; 1]
 1
 [2]
-(mk_rewrite true (Node(zz, "APPLIST", [Nvar(zz, "plus_permute");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
+(mk_rewrite true (mkAppC(mk_id( "plus_permute"),[(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
 
 add_dad_rule "plus-permute-rl"
-(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])]))
+(mkAppC(mk_id("plus"),[mkMetaC(4);mkAppC(mk_id("plus"),[mkMetaC(3);mkMetaC(2)])]))
 [2; 2; 2; 1]
 [2; 1]
 1
 [2]
-(mk_rewrite true (Node(zz, "APPLIST", [Nvar(zz, "plus_permute");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));;
+(mk_rewrite true (mkAppC(mk_id( "plus_permute"),[(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));;
 
 vinterp_add "StartDad"
    (function
diff --git a/contrib/interface/dad.mli b/contrib/interface/dad.mli
index dc2b2734cd..f556c19267 100644
--- a/contrib/interface/dad.mli
+++ b/contrib/interface/dad.mli
@@ -1,10 +1,10 @@
 open Proof_type;;
 open Tacmach;;
-
+open Topconstr;;
 
 val dad_rule_names : unit -> string list;;
 val start_dad : unit -> unit;;
 val dad_tac : (Tacexpr.raw_tactic_expr -> 'a) -> int list -> int list -> goal sigma ->
                   goal list sigma * validation;;
-val add_dad_rule : string -> Ctast.t -> (int list) -> (int list) ->
+val add_dad_rule : string -> constr_expr -> (int list) -> (int list) ->
                    int -> (int list) -> Tacexpr.raw_atomic_tactic_expr -> unit;;
diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4
index b4db228030..343f90d6e5 100644
--- a/contrib/interface/debug_tac.ml4
+++ b/contrib/interface/debug_tac.ml4
@@ -279,7 +279,7 @@ let mkOnThen t1 t2 selected_indices =
   let a = in_gen rawwit_tactic t1 in
   let b = in_gen rawwit_tactic t2 in
   let l = in_gen (wit_list0 rawwit_int) selected_indices in
-  TacAtom (dummy_loc, TacExtend ("OnThen", [a;b;l]));;
+  TacAtom (dummy_loc, TacExtend (dummy_loc, "OnThen", [a;b;l]));;
 
 (* Analyzing error reports *)
 
@@ -363,7 +363,7 @@ let rec reconstruct_success_tac tac =
 	  Report_node(true, n, l) -> tac
 	| Report_node(false, n, rl) ->
 	    let selected_indices = select_success 1 rl in
-	    TacAtom (Ast.dummy_loc,TacExtend ("OnThen",
+	    TacAtom (dummy_loc,TacExtend (dummy_loc,"OnThen",
 	      [in_gen rawwit_tactic a;
 	       in_gen rawwit_tactic b;
 	       in_gen (wit_list0 rawwit_int) selected_indices]))
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index ec600d21dc..a7e1f34449 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -20,6 +20,7 @@ open Declare;;
 open Nametab
 open Vernacexpr;;
 open Decl_kinds;;
+open Constrextern;;
 
 (* This function converts the parameter binders of an inductive definition,
    in particular you have to be careful to handle each element in the
@@ -28,7 +29,7 @@ open Decl_kinds;;
 let convert_env =
     let convert_binder env (na, _, c) =
       match na with 
-       | Name id -> (id, ast_of_constr true env c)
+       | Name id -> (id, extern_constr true env c)
        | Anonymous -> failwith "anomaly: Anonymous variables in inductives" in
     let rec cvrec env = function
        [] -> []
@@ -102,7 +103,7 @@ let convert_constructors envpar names types =
     array_map2 
       (fun n t -> 
 	let coercion_flag = false (* arbitrary *) in
-	(coercion_flag, (n, ast_of_constr true envpar t)))
+	(coercion_flag, (n, extern_constr true envpar t)))
       names types in
   Array.to_list array_idC;;
   
@@ -116,7 +117,7 @@ let convert_one_inductive sp tyi =
   let sp = sp_of_global None (IndRef (sp, tyi)) in
   (basename sp,
    convert_env(List.rev params),
-   (ast_of_constr true envpar arity),
+   (extern_constr true envpar arity),
    convert_constructors envpar cstrnames cstrtypes);;
 
 (* This function converts a Mutual inductive definition to a Coqast.t.
@@ -132,7 +133,7 @@ let mutual_to_ast_list sp mib =
   :: (implicit_args_to_ast_list sp mipv);;
 
 let constr_to_ast v = 
-  ast_of_constr true (Global.env()) v;;
+  extern_constr true (Global.env()) v;;
 
 let implicits_to_ast_list implicits =
   match (impl_args_to_string implicits) with
@@ -215,7 +216,8 @@ let leaf_entry_to_ast_list ((sp,kn),lobj) =
 
 
 (* this function is inspired by print_name *)
-let name_to_ast qid = 
+let name_to_ast ref =
+  let (loc,qid) = qualid_of_reference ref in
   let l = 
     try
       let sp = Nametab.locate_obj qid in
diff --git a/contrib/interface/name_to_ast.mli b/contrib/interface/name_to_ast.mli
index 600ec5f918..0eca0a1e77 100644
--- a/contrib/interface/name_to_ast.mli
+++ b/contrib/interface/name_to_ast.mli
@@ -1,2 +1,2 @@
-val name_to_ast : Libnames.qualid -> Vernacexpr.vernac_expr;;
+val name_to_ast : Libnames.reference -> Vernacexpr.vernac_expr;;
 val convert_qualid : Libnames.qualid -> Coqast.t;;
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 61fd060724..a8d74c30e1 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -112,7 +112,7 @@ let execute_when_necessary v =
       (try 
 	Vernacentries.interp v
        with _ ->
-	 let l=prlist_with_sep spc (fun (_,qid) -> pr_qualid qid) l in
+	 let l=prlist_with_sep spc pr_reference l in
 	 msgnl (str "Reinterning of " ++ l ++ str " failed"))
   | VernacRequireFrom (_,_,name,_) ->
       (try 
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 7bd29a9584..469a067f44 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -17,6 +17,10 @@ open Tacmach;;
 open Tacexpr;;
 open Typing;;
 open Pp;;
+open Libnames;;
+open Topconstr;;
+
+let zz = (0,0);;
 
 (* get_hyp_by_name : goal sigma -> string -> constr,
    looks up for an hypothesis (or a global constant), from its name *)
@@ -25,13 +29,12 @@ let get_hyp_by_name g name =
   let env = pf_env g in
   try (let judgment = 
          Pretyping.understand_judgment 
-          evd env (RVar(dummy_loc, name)) in
+          evd env (RVar(zz, name)) in
        ("hyp",judgment.uj_type))
 (* je sais, c'est pas beau, mais je ne sais pas trop me servir de look_up...
    Loïc *)
-  with _ -> (let ast = Termast.ast_of_qualid (Libnames.make_short_qualid name)in
-             let c = Astterm.interp_constr evd env ast in
-             ("cste",type_of (Global.env()) Evd.empty c))
+  with _ -> (let c = Nametab.global (Ident (zz,name)) in
+             ("cste",type_of (Global.env()) Evd.empty (constr_of_reference c)))
 ;;
 
 type pbp_atom =
@@ -85,8 +88,6 @@ type pbp_rule = (identifier list *
                        identifier option -> (types, constr) kind_of_term -> int list -> pbp_sequence)) ->
                     pbp_sequence option;;
 
-let zz = (0,0);;
-
 (*
 let make_named_intro s =
     Node(zz, "Intros",
@@ -164,10 +165,13 @@ let (imply_intro1: pbp_rule) = function
 		(kind_of_term prem) path))
   | _ -> None;;
 
+let make_var id = CRef (Ident(zz, id))
+
+let make_app f l = CApp (zz,f,List.map (fun x -> (x,None)) l)
+
 let make_pbp_pattern x =
-  Coqast.Node(zz,"APPLIST",
-    [Coqast.Nvar (zz, id_of_string "PBP_META");
-     Coqast.Nvar (zz, id_of_string ("Value_for_" ^ (string_of_id x)))])
+  make_app (make_var (id_of_string "PBP_META"))
+     [make_var (id_of_string ("Value_for_" ^ (string_of_id x)))]
 
 let rec make_then = function
   | [] -> TacId
@@ -177,26 +181,26 @@ let rec make_then = function
 let make_pbp_atomic_tactic = function
   | PbpTryAssumption None -> TacTry (TacAtom (zz, TacAssumption))
   | PbpTryAssumption (Some a) ->
-      TacTry (TacAtom (zz, TacExact (Coqast.Nvar (zz,a))))
+      TacTry (TacAtom (zz, TacExact (make_var a)))
   | PbpExists x -> 
       TacAtom (zz, TacSplit (ImplicitBindings [make_pbp_pattern x]))
   | PbpGeneralize (h,args) ->
-      let l = Coqast.Nvar (zz, h)::List.map make_pbp_pattern args in
-      TacAtom (zz, TacGeneralize [Coqast.Node (zz, "APPLIST", l)])
+      let l = List.map make_pbp_pattern args in
+      TacAtom (zz, TacGeneralize [make_app (make_var h) l])
   | PbpLeft -> TacAtom (zz, TacLeft NoBindings)
   | PbpRight -> TacAtom (zz, TacRight NoBindings)
   | PbpReduce -> TacAtom (zz, TacReduce (Red false, []))
   | PbpIntros l -> 
       let l = List.map (fun id -> IntroIdentifier id) l in
       TacAtom (zz, TacIntroPattern l)
-  | PbpLApply h -> TacAtom (zz, TacLApply (Coqast.Nvar (zz, h)))
-  | PbpApply h -> TacAtom (zz, TacApply (Coqast.Nvar(zz, h),NoBindings))
+  | PbpLApply h -> TacAtom (zz, TacLApply (make_var h))
+  | PbpApply h -> TacAtom (zz, TacApply (make_var h,NoBindings))
   | PbpElim (hyp_name, names) ->
       let bind = List.map (fun s -> (NamedHyp s,make_pbp_pattern s)) names in
       TacAtom
-	(zz, TacElim ((Coqast.Nvar(zz,hyp_name),ExplicitBindings bind),None))
+	(zz, TacElim ((make_var hyp_name,ExplicitBindings bind),None))
   | PbpTryClear l -> 
-      TacTry (TacAtom (zz, TacClear (List.map (fun s -> AN (zz,s)) l)))
+      TacTry (TacAtom (zz, TacClear (List.map (fun s -> AN s) l)))
   | PbpSplit -> TacAtom (zz, TacSplit NoBindings);;
 
 let rec make_pbp_tactic = function
@@ -254,7 +258,7 @@ let reference dir s =
     anomaly ("Coqlib: cannot find "^
 	     (Libnames.string_of_qualid (Libnames.make_qualid dir id)))
 
-let constant dir s =  Declare.constr_of_reference (reference dir s);;
+let constant dir s =  constr_of_reference (reference dir s);;
 
 let andconstr: unit -> constr = Coqlib.build_coq_and;;
 let prodconstr () = constant "Datatypes" "prod";;
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index c7e6be1318..4ae1f280d6 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -17,7 +17,6 @@ open Translate
 open Term
 open Reductionops
 open Clenv
-open Astterm
 open Typing
 open Inductive
 open Inductiveops
@@ -188,8 +187,8 @@ let rule_to_ntactic r =
    let rt =
      (match r with
        Tactic (t,_) -> t
-     | Prim (Refine h) -> TacAtom (Ast.dummy_loc,TacExact h)
-     | _ -> TacAtom (Ast.dummy_loc, TacIntroPattern [])) in
+     | Prim (Refine h) -> TacAtom (dummy_loc,TacExact h)
+     | _ -> TacAtom (dummy_loc, TacIntroPattern [])) in
    if rule_is_complex r
    then (match rt with
            TacArg (Tacexp _) as t -> t
@@ -198,12 +197,13 @@ let rule_to_ntactic r =
    else rt
 ;;
 
-
+(*
 let term_of_command x =
   match x with
     Node(_,_,y::_) -> y
   | _ -> x
 ;;
+*)
 
 (* Attribue les preuves de la liste l aux sous-buts non-prouvés de nt  *)
 
@@ -270,7 +270,7 @@ let  to_nproof sigma osign pf =
 			    t_concl=concl ntree;
 			    t_full_concl=ntree.t_goal.t_full_concl;
 			    t_full_env=ntree.t_goal.t_full_env};
-		  t_proof= Proof (TacAtom (Ast.dummy_loc,TacExtend ("InfoAuto",[])), [ntree])}
+		  t_proof= Proof (TacAtom (dummy_loc,TacExtend (dummy_loc,"InfoAuto",[])), [ntree])}
 	      else ntree
 	  | _ -> ntree))
       	else
@@ -415,7 +415,7 @@ let enumerate f ln =
 ;;
 
 
-let constr_of_ast = Astterm.interp_constr Evd.empty (Global.env());;
+let constr_of_ast = Constrintern.interp_constr Evd.empty (Global.env());;
 
 (*
 let sp_tac tac =
@@ -1139,7 +1139,7 @@ let eq_term = eq_constr;;
 let is_equality_tac = function
   | TacAtom (_,
       (TacExtend
-	(("ERewriteLR"|"ERewriteRL"|"ERewriteLRocc"|"ERewriteRLocc"
+	(_,("ERewriteLR"|"ERewriteRL"|"ERewriteLRocc"|"ERewriteRLocc"
 	 |"ERewriteParallel"|"ERewriteNormal"
 	 |"RewriteLR"|"RewriteRL"|"Replace"),_)
       | TacReduce _
@@ -1196,7 +1196,7 @@ let  list_to_eq l o=
 
 let stde = Global.env;;
 
-let dbize env = Astterm.interp_constr Evd.empty env;;
+let dbize env = Constrintern.interp_constr Evd.empty env;;
 
 (**********************************************************************)
 let rec natural_ntree ig ntree =
@@ -1214,8 +1214,7 @@ let rec natural_ntree ig ntree =
 	(fun (_,ntree) ->
 	 let lemma =  match (proof ntree) with
 	   Proof (tac,ltree) ->
-	     (try (sph [spt (dbize (gLOB ge)
-				(term_of_command (arg1_tactic tac)));(* TODO *)
+	     (try (sph [spt (dbize (gLOB ge) (arg1_tactic tac));(* TODO *)
 			  (match ltree with
 			    [] ->spe
 			  | [_] -> spe
@@ -1279,39 +1278,39 @@ let rec natural_ntree ig ntree =
 	  | TacLeft _ -> natural_left ig lh g gs ltree
 	  | (* "Simpl" *)TacReduce (r,cl)  ->
 	      natural_reduce ig lh g gs ge r cl ltree
-	  | TacExtend ("InfoAuto",[]) -> natural_infoauto ig lh g gs ltree
+	  | TacExtend (_,"InfoAuto",[]) -> natural_infoauto ig lh g gs ltree
 	  | TacAuto _ -> natural_auto ig lh g gs ltree
-	  | TacExtend ("EAuto",_) -> natural_auto ig lh g gs ltree
+	  | TacExtend (_,"EAuto",_) -> natural_auto ig lh g gs ltree
 	  | TacTrivial _ -> natural_trivial ig lh g gs ltree
 	  | TacAssumption -> natural_trivial ig lh g gs ltree
 	  | TacClear _ -> natural_clear ig lh g gs ltree
 (* Besoin de l'argument de la tactique *)
 	  | TacOldInduction (NamedHyp id) -> 
               natural_induction ig lh g gs ge id ltree false
-	  | TacExtend ("InductionIntro",[a]) -> 
+	  | TacExtend (_,"InductionIntro",[a]) -> 
               let id=(out_gen wit_ident a) in
               natural_induction ig lh g gs ge id ltree true
 	  | TacApply (c,_) -> natural_apply ig lh g gs c ltree
 	  | TacExact c -> natural_exact ig lh g gs c ltree
 	  | TacCut c -> natural_cut ig lh g gs c ltree
-	  | TacExtend ("CutIntro",[a]) ->
+	  | TacExtend (_,"CutIntro",[a]) ->
 	      let c = out_gen wit_constr a in
 	      natural_cutintro ig lh g gs a ltree
 	  | TacCase (c,_) -> natural_case ig lh g gs ge c ltree false
-	  | TacExtend ("CaseIntro",[a]) ->
+	  | TacExtend (_,"CaseIntro",[a]) ->
 	      let c = out_gen wit_constr a in
 	      natural_case ig lh g gs ge c ltree true
 	  | TacElim ((c,_),_) -> natural_elim ig lh g gs ge c ltree false
-	  | TacExtend ("ElimIntro",[a]) ->
+	  | TacExtend (_,"ElimIntro",[a]) ->
 	      let c = out_gen wit_constr a in
 	      natural_elim ig lh g gs ge c ltree true
-	  | TacExtend ("Rewrite",[_;a]) ->
+	  | TacExtend (_,"Rewrite",[_;a]) ->
 	      let (c,_) = out_gen wit_constr_with_bindings a in
 	      natural_rewrite ig lh g gs c ltree
-	  | TacExtend ("ERewriteRL",[a]) ->
+	  | TacExtend (_,"ERewriteRL",[a]) ->
 	      let c = out_gen wit_constr a in (* TODO *)
 	      natural_rewrite ig lh g gs c ltree
-	  | TacExtend ("ERewriteLR",[a]) ->
+	  | TacExtend (_,"ERewriteLR",[a]) ->
 	      let c = out_gen wit_constr a in (* TODO *)
 	      natural_rewrite ig lh g gs c ltree
 	  |_ -> natural_generic ig lh g gs (sps (name_tactic tac)) (prl sp_tac [tac]) ltree
diff --git a/contrib/interface/showproof.mli b/contrib/interface/showproof.mli
index c84642d775..ee2694585f 100755
--- a/contrib/interface/showproof.mli
+++ b/contrib/interface/showproof.mli
@@ -10,7 +10,6 @@ open Translate
 open Term
 open Reduction
 open Clenv
-open Astterm
 open Typing
 open Inductive
 open Vernacinterp
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 92a35b892e..a5a153bdb7 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -13,6 +13,8 @@ open Rawterm;;
 open Tacexpr;;
 open Vernacexpr;;
 open Decl_kinds;;
+open Topconstr;;
+open Libnames;;
 
 let in_coq_ref = ref false;;
 
@@ -297,23 +299,25 @@ let qualid_to_ct_ID =
     | Node(_, "QUALIDMETA",[Num(_,n)]) -> Some(CT_metac (CT_int n))
     | _ -> None;;
 
-let tac_qualid_to_ct_ID qid = CT_ident (Libnames.string_of_qualid qid)
+let tac_qualid_to_ct_ID ref = 
+  CT_ident (Libnames.string_of_qualid (snd (qualid_of_reference ref)))
 
-let loc_qualid_to_ct_ID (_,qid) = CT_ident (Libnames.string_of_qualid qid)
+let loc_qualid_to_ct_ID ref =
+  CT_ident (Libnames.string_of_qualid (snd (qualid_of_reference ref)))
 
 let qualid_or_meta_to_ct_ID = function
-  | AN (_,qid) -> tac_qualid_to_ct_ID qid
+  | AN qid -> tac_qualid_to_ct_ID qid
   | MetaNum (_,n) -> CT_metac (CT_int n)
 
 let ident_or_meta_to_ct_ID = function
-  | AN (_,id) -> xlate_ident id
+  | AN id -> xlate_ident id
   | MetaNum (_,n) -> CT_metac (CT_int n)
 
 let xlate_qualid_list l = CT_id_list (List.map loc_qualid_to_ct_ID l)
 
 let reference_to_ct_ID = function
-  | Coqast.RIdent (_,id) -> CT_ident (Names.string_of_id id)
-  | Coqast.RQualid (_,qid) -> CT_ident (Libnames.string_of_qualid qid)
+  | Ident (_,id) -> CT_ident (Names.string_of_id id)
+  | Qualid (_,qid) -> CT_ident (Libnames.string_of_qualid qid)
 
 let xlate_class = function
   | FunClass -> CT_ident "FUNCLASS"
@@ -755,10 +759,10 @@ let xlate_special_cases cont_function arg =
 
 let xlate_sort =
   function
-    | Coqast.Node (_, "SET", []) -> CT_sortc "Set"
-    | Coqast.Node (_, "PROP", []) -> CT_sortc "Prop"
-    | Coqast.Node (_, "TYPE", []) -> CT_sortc "Type"
-    | _ -> xlate_error "xlate_sort";;
+    | RProp Term.Pos -> CT_sortc "Set"
+    | RProp Term.Null -> CT_sortc "Prop"
+    | RType None -> CT_sortc "Type"
+    | RType (Some u) -> xlate_error "xlate_sort";;
 
 let xlate_formula a =
   !set_flags ();
@@ -986,7 +990,7 @@ and (xlate_call_or_tacarg:raw_tactic_arg -> ct_TACTIC_COM) =
 	CT_simple_user_tac
 	  (reference_to_ct_ID r,
 	    CT_tactic_arg_list(xlate_tacarg a,List.map xlate_tacarg l))
-    | Reference (Coqast.RIdent (_,s)) -> ident_tac s
+    | Reference (Ident (_,s)) -> ident_tac s
     | t -> xlate_error "TODO: result other than tactic or constr"
 
 and xlate_red_tactic =
@@ -1103,21 +1107,21 @@ and xlate_tactic =
 
 and xlate_tac =
   function
-    | TacExtend ("Absurd",[c]) ->
+    | TacExtend (_,"Absurd",[c]) ->
        CT_absurd (xlate_constr (out_gen rawwit_constr c))
     | TacChange (f, b) -> CT_change (xlate_constr f, xlate_clause b)
-    | TacExtend ("Contradiction",[]) -> CT_contradiction
+    | TacExtend (_,"Contradiction",[]) -> CT_contradiction
     | TacDoubleInduction (AnonHyp n1, AnonHyp n2) ->
 	CT_tac_double (CT_int n1, CT_int n2)
     | TacDoubleInduction _ -> xlate_error "TODO: Double Induction id1 id2"
-    | TacExtend ("Discriminate", [idopt]) ->
+    | TacExtend (_,"Discriminate", [idopt]) ->
      CT_discriminate_eq
          (xlate_quantified_hypothesis_opt
 	    (out_gen (wit_opt rawwit_quant_hyp) idopt))
-    | TacExtend ("DEq", [idopt]) ->
+    | TacExtend (_,"DEq", [idopt]) ->
      CT_simplify_eq
          (xlate_ident_opt (out_gen (wit_opt rawwit_ident) idopt))
-    | TacExtend ("Injection", [idopt]) ->
+    | TacExtend (_,"Injection", [idopt]) ->
      CT_injection_eq
          (xlate_quantified_hypothesis_opt
 	    (out_gen (wit_opt rawwit_quant_hyp) idopt))
@@ -1153,32 +1157,32 @@ and xlate_tac =
     | TacLeft bindl -> CT_left (xlate_bindings bindl)
     | TacRight bindl -> CT_right (xlate_bindings bindl)
     | TacSplit bindl -> CT_split (xlate_bindings bindl)
-    | TacExtend ("Replace", [c1; c2]) ->
+    | TacExtend (_,"Replace", [c1; c2]) ->
      let c1 = xlate_constr (out_gen rawwit_constr c1) in
      let c2 = xlate_constr (out_gen rawwit_constr c2) in
      CT_replace_with (c1, c2)
     |
-      TacExtend ("Rewrite", [b; cbindl]) ->
+      TacExtend (_,"Rewrite", [b; cbindl]) ->
      let b = out_gen Extraargs.rawwit_orient b in
      let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
      let c = xlate_constr c and bindl = xlate_bindings bindl in
      if b then CT_rewrite_lr (c, bindl, ctv_ID_OPT_NONE)
      else CT_rewrite_rl (c, bindl, ctv_ID_OPT_NONE)
-    | TacExtend ("RewriteIn", [b; cbindl; id]) ->
+    | TacExtend (_,"RewriteIn", [b; cbindl; id]) ->
      let b = out_gen Extraargs.rawwit_orient b in
      let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
      let c = xlate_constr c and bindl = xlate_bindings bindl in
      let id = ctf_ID_OPT_SOME (xlate_ident (out_gen rawwit_ident id)) in
      if b then CT_rewrite_lr (c, bindl, id)
      else CT_rewrite_rl (c, bindl, id)
-    | TacExtend ("ConditionalRewrite", [t; b; cbindl]) ->
+    | TacExtend (_,"ConditionalRewrite", [t; b; cbindl]) ->
      let t = out_gen rawwit_tactic t in
      let b = out_gen Extraargs.rawwit_orient b in
      let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
      let c = xlate_constr c and bindl = xlate_bindings bindl in
      if b then CT_condrewrite_lr (xlate_tactic t, c, bindl, ctv_ID_OPT_NONE)
      else CT_condrewrite_rl (xlate_tactic t, c, bindl, ctv_ID_OPT_NONE)
-    | TacExtend ("ConditionalRewriteIn", [t; b; cbindl; id]) ->
+    | TacExtend (_,"ConditionalRewriteIn", [t; b; cbindl; id]) ->
      let t = out_gen rawwit_tactic t in
      let b = out_gen Extraargs.rawwit_orient b in
      let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
@@ -1186,7 +1190,7 @@ and xlate_tac =
      let id = ctf_ID_OPT_SOME (xlate_ident (out_gen rawwit_ident id)) in
      if b then CT_condrewrite_lr (xlate_tactic t, c, bindl, id)
      else CT_condrewrite_rl (xlate_tactic t, c, bindl, id)
-    | TacExtend ("DependentRewrite", [b; id_or_constr]) ->
+    | TacExtend (_,"DependentRewrite", [b; id_or_constr]) ->
       let b = out_gen Extraargs.rawwit_orient b in
       (match genarg_tag id_or_constr with
 	| IdentArgType -> (*Dependent Rewrite/SubstHypInConcl*)
@@ -1197,7 +1201,7 @@ and xlate_tac =
 	    if b then CT_cutrewrite_lr (c, ctv_ID_OPT_NONE)
 	    else CT_cutrewrite_rl (c, ctv_ID_OPT_NONE)
 	| _ -> xlate_error "")
-    | TacExtend ("DependentRewrite", [b; c; id]) -> (*CutRewrite in/SubstHyp*)
+    | TacExtend (_,"DependentRewrite", [b; c; id]) -> (*CutRewrite in/SubstHyp*)
       let b = out_gen Extraargs.rawwit_orient b in
       let c = xlate_constr (out_gen rawwit_constr c) in
       let id = xlate_ident (out_gen rawwit_ident id) in
@@ -1224,7 +1228,7 @@ and xlate_tac =
 	CT_auto_with(xlate_int_opt nopt,
              CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
              CT_id_ne_list(CT_ident id1, List.map (fun x -> CT_ident x) idl)))
-    | TacExtend ("EAuto", [nopt; popt; idl]) ->
+    | TacExtend (_,"EAuto", [nopt; popt; idl]) ->
 	let first_n =
 	  match out_gen (wit_opt rawwit_int_or_var) nopt with
 	    | Some (ArgVar(_, s)) -> xlate_id_to_id_or_int_opt s
@@ -1245,12 +1249,12 @@ and xlate_tac =
 			      (CT_id_ne_list
 				 (CT_ident a,
 				  List.map (fun x -> CT_ident x) l))))
-    | TacExtend ("Prolog", [cl; n]) ->
+    | TacExtend (_,"Prolog", [cl; n]) ->
       let cl = List.map xlate_constr (out_gen (wit_list0 rawwit_constr) cl) in
       (match out_gen wit_int_or_var n with
 	| ArgVar _ -> xlate_error ""
 	| ArgArg n -> CT_prolog (CT_formula_list cl, CT_int  n))
-    | TacExtend ("EApply", [cbindl]) ->
+    | TacExtend (_,"EApply", [cbindl]) ->
      let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
      let c = xlate_constr c and bindl = xlate_bindings bindl in
      CT_eapply (c, bindl)
@@ -1302,11 +1306,12 @@ and xlate_tac =
        let idl' = List.map ident_or_meta_to_ct_ID idl in
        CT_clear (CT_id_ne_list (ident_or_meta_to_ct_ID id, idl'))
     | (*For translating tactics/Inv.v *)
-      TacExtend ("SimpleInversion"|"Inversion"|"InversionClear" as s, [id]) ->
+      TacExtend (_,("SimpleInversion"|"Inversion"|"InversionClear" as s), [id])
+      ->
 	let quant_hyp =  out_gen rawwit_quant_hyp id in
 	  CT_inversion(compute_INV_TYPE_from_string s,
 		       xlate_quantified_hypothesis quant_hyp, CT_id_list [])
-    | TacExtend ("SimpleInversion"|"Inversion"|"InversionClear" as s,
+    | TacExtend (_,("SimpleInversion"|"Inversion"|"InversionClear" as s),
         [id;copt_or_idl]) ->
 	let quant_hyp = (out_gen rawwit_quant_hyp id) in
 	let id = xlate_quantified_hypothesis quant_hyp in
@@ -1320,17 +1325,17 @@ and xlate_tac =
 	      CT_depinversion
 		(compute_INV_TYPE_from_string s, id, xlate_constr_opt copt)
 	  | _ -> xlate_error "")
-    | TacExtend ("InversionUsing", [id; c]) ->
+    | TacExtend (_,"InversionUsing", [id; c]) ->
      let id = xlate_quantified_hypothesis (out_gen rawwit_quant_hyp id) in
      let c = out_gen rawwit_constr c in
      CT_use_inversion (id, xlate_constr c, CT_id_list [])
-    | TacExtend ("InversionUsing", [id; c; idlist]) ->
+    | TacExtend (_,"InversionUsing", [id; c; idlist]) ->
      let id = xlate_quantified_hypothesis (out_gen rawwit_quant_hyp id) in
      let c = out_gen rawwit_constr c in
      let idlist = out_gen (wit_list1 rawwit_ident) idlist in
      CT_use_inversion (id, xlate_constr c,
        CT_id_list (List.map xlate_ident idlist))
-    | TacExtend ("Omega", []) -> CT_omega
+    | TacExtend (_,"Omega", []) -> CT_omega
     | TacRename (_, _) -> xlate_error "TODO: Rename id into id'"
     | TacClearBody _ -> xlate_error "TODO: Clear Body H"
     | TacDAuto (_, _) -> xlate_error "TODO: DAuto"
@@ -1341,7 +1346,7 @@ and xlate_tac =
     | TacForward (_, _, _) -> xlate_error "TODO: Assert/Pose id:=c"
     | TacTrueCut (_, _) -> xlate_error "TODO: Assert id:t"
     | TacAnyConstructor tacopt -> xlate_error "TODO: Constructor tac"
-    | TacExtend (id, l) ->
+    | TacExtend (_,id, l) ->
      CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l))
     | TacAlias (_, _, _) -> xlate_error "TODO: aliases"
 
@@ -1366,10 +1371,13 @@ and coerce_genarg_to_TARG x =
   | IdentArgType ->
       let id = xlate_ident (out_gen rawwit_ident x) in
       CT_coerce_ID_OR_INT_to_TARG (CT_coerce_ID_to_ID_OR_INT id)
-  | QualidArgType ->
-      let id = tac_qualid_to_ct_ID (snd (out_gen rawwit_qualid x)) in
+  | RefArgType ->
+      let id = tac_qualid_to_ct_ID (out_gen rawwit_ref x) in
       CT_coerce_ID_OR_INT_to_TARG (CT_coerce_ID_to_ID_OR_INT id)
   (* Specific types *)
+  | SortArgType ->
+      CT_coerce_FORMULA_to_TARG
+        (CT_coerce_SORT_TYPE_to_FORMULA (xlate_sort (out_gen rawwit_sort x)))
   | ConstrArgType ->
       CT_coerce_FORMULA_to_TARG (xlate_constr (out_gen rawwit_constr x))
   | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
@@ -1440,12 +1448,16 @@ let coerce_genarg_to_VARG x =
       CT_coerce_ID_OPT_OR_ALL_to_VARG
 	      (CT_coerce_ID_OPT_to_ID_OPT_OR_ALL
 	        (CT_coerce_ID_to_ID_OPT id))
-  | QualidArgType ->
-      let id = tac_qualid_to_ct_ID (snd (out_gen rawwit_qualid x)) in
+  | RefArgType ->
+      let id = tac_qualid_to_ct_ID (out_gen rawwit_ref x) in
       CT_coerce_ID_OPT_OR_ALL_to_VARG
 	      (CT_coerce_ID_OPT_to_ID_OPT_OR_ALL
 	        (CT_coerce_ID_to_ID_OPT id))
   (* Specific types *)
+  | SortArgType ->
+     CT_coerce_FORMULA_OPT_to_VARG 
+      (CT_coerce_FORMULA_to_FORMULA_OPT
+	(CT_coerce_SORT_TYPE_to_FORMULA (xlate_sort (out_gen rawwit_sort x))))
   | ConstrArgType ->
      CT_coerce_FORMULA_OPT_to_VARG 
       (CT_coerce_FORMULA_to_FORMULA_OPT (xlate_constr (out_gen rawwit_constr x)))
@@ -1580,6 +1592,18 @@ let cvt_vernac_binder = function
 let cvt_vernac_binders args =
   CT_binder_list(List.map cvt_vernac_binder args)
 
+let cvt_name = function
+  | (_,Name id) -> xlate_ident_opt (Some id)
+  | (_,Anonymous) -> xlate_ident_opt None
+
+let cvt_fixpoint_binder = function
+  | (na::l,c) ->
+     CT_binder(CT_id_opt_ne_list (cvt_name na,List.map cvt_name l),
+       xlate_constr c)
+  | [],c -> xlate_error "Shouldn't occur"
+
+let cvt_fixpoint_binders args =
+  CT_binder_list(List.map cvt_fixpoint_binder args)
 
 let xlate_vernac =
  function
@@ -1642,7 +1666,8 @@ let xlate_vernac =
        (CT_string_ne_list (CT_string str, List.map (fun x -> CT_string x) l))
     | VernacGoal c ->
 	CT_coerce_THEOREM_GOAL_to_COMMAND (CT_goal (xlate_constr c))
-    | VernacAbort (Some id) -> CT_abort(ctf_ID_OPT_OR_ALL_SOME(xlate_ident id))
+    | VernacAbort (Some (_,id)) ->
+	CT_abort(ctf_ID_OPT_OR_ALL_SOME(xlate_ident id))
     | VernacAbort None -> CT_abort ctv_ID_OPT_OR_ALL_NONE
     | VernacAbortAll -> CT_abort ctv_ID_OPT_OR_ALL_ALL
     | VernacRestart -> CT_restart
@@ -1681,10 +1706,7 @@ let xlate_vernac =
 	    CT_hint(xlate_ident id_name, dblist,
               CT_extern(CT_int n, xlate_constr c, xlate_tactic t))
      | HintsResolve l -> (* = Old HintsResolve *)
-	 let l = List.map
-	   (function
-	       (None,Coqast.Node(_,"QUALID",l)) -> Astterm.interp_qualid l
-	     | _ -> failwith "") l in
+	 let l = List.map (function (None,CRef r) -> r | _ -> failwith "") l in
 	 let n1, names = match List.map tac_qualid_to_ct_ID l with
 	     n1 :: names -> n1, names
 	   | _  -> failwith "" in
@@ -1692,10 +1714,7 @@ let xlate_vernac =
                   CT_id_ne_list(n1, names),
 		  dblist)
      | HintsImmediate l -> (* = Old HintsImmediate *)
-	 let l = List.map
-	   (function
-	       (None,Coqast.Node(_,"QUALID",l)) -> Astterm.interp_qualid l
-	     | _ -> failwith "") l in
+	 let l = List.map (function (None,CRef r) -> r | _ -> failwith "") l in
 	 let n1, names = match List.map tac_qualid_to_ct_ID l with
 	     n1 :: names -> n1, names
 	   | _  -> failwith "" in
@@ -1705,7 +1724,7 @@ let xlate_vernac =
      | HintsUnfold l ->  (* = Old HintsUnfold *)
 	 let l = List.map
 	   (function
-	       (None,qid) -> loc_qualid_to_ct_ID qid
+	       (None,ref) -> loc_qualid_to_ct_ID ref
 	     | _ -> failwith "") l in
 	 let n1, names = match l with
 	     n1 :: names -> n1, names
@@ -1780,7 +1799,7 @@ let xlate_vernac =
   | VernacStartTheoremProof (k, s, (bl,c), _, _) -> 
       xlate_error "TODO: VernacStartTheoremProof"
   | VernacSuspend -> CT_suspend
-  | VernacResume idopt -> CT_resume (xlate_ident_opt idopt)
+  | VernacResume idopt -> CT_resume (xlate_ident_opt (option_app snd idopt))
   | VernacDefinition (k,s,ProveBody (bl,typ),_) ->
       if bl <> [] then xlate_error "TODO: Def bindings";
       CT_coerce_THEOREM_GOAL_to_COMMAND(
@@ -1854,7 +1873,7 @@ let xlate_vernac =
    | VernacFixpoint [] -> xlate_error "mutual recursive"
    | VernacFixpoint (lm :: lmi) ->
       let strip_mutrec (fid, bl, arf, ardef) =
-	match cvt_vernac_binders bl with
+	match cvt_fixpoint_binders bl with
 	  | CT_binder_list (b :: bl) ->
 	      CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl),
 	        xlate_constr arf, xlate_constr ardef)
@@ -1907,6 +1926,8 @@ let xlate_vernac =
 
    | VernacNotation _ -> xlate_error "TODO: Notation"
 
+   | VernacSyntaxExtension _ -> xlate_error "Syntax Extension not implemented"
+
    | VernacInfix (str_assoc, n, str, id, None) ->
       CT_infix (
        (match str_assoc with
@@ -1936,7 +1957,7 @@ let xlate_vernac =
        | Local -> CT_local in
       CT_coercion (local_opt, id_opt, xlate_ident id1,
         xlate_class id2, xlate_class id3)
-  | VernacResetName id -> CT_reset (xlate_ident id)
+  | VernacResetName id -> CT_reset (xlate_ident (snd id))
   | VernacResetInitial -> CT_restore_state (CT_ident "Initial")
   | VernacExtend (s, l) ->
       CT_user_vernac
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index db9b00c384..f4848c729e 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -36,7 +36,7 @@ open Nametab
 open Quote
 
 let mt_evd = Evd.empty
-let constr_of c = Astterm.interp_constr mt_evd (Global.env()) c
+let constr_of c = Constrintern.interp_constr mt_evd (Global.env()) c
 
 let constant dir s =
   let dir = make_dirpath (List.map id_of_string (List.rev ("Coq"::dir))) in
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 19dfc940ae..1cd33f53c4 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -249,7 +249,7 @@ print_endline "PASSATO" ; flush stdout ;
           let subst,residual_args,uninst_vars =
            let variables,basedir =
              try
-               let g = Declare.reference_of_constr h in
+               let g = Libnames.reference_of_constr h in
                let sp =
                 match g with
                    Libnames.ConstructRef ((induri,_),_)
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 151d4582b9..07df70a0c0 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -393,7 +393,7 @@ let mk_inductive_obj sp packs variables hyps finite =
 (* Note: it is printed only (and directly) the most cooked available      *)
 (*       form of the definition (all the parameters are                   *)
 (*       lambda-abstracted, but the object can still refer to variables)  *)
-let print (_,qid as locqid) fn =
+let print r fn =
  let module D = Declarations in
  let module De = Declare in
  let module G = Global in
@@ -402,14 +402,16 @@ let print (_,qid as locqid) fn =
  let module T = Term in
  let module X = Xml in
  let module Ln = Libnames in
-  let (_,id) = Libnames.repr_qualid qid in
+  let (_,id) = Ln.repr_qualid (snd (Ln.qualid_of_reference r)) in
   let glob_ref =
 (*CSC: ask Hugo why Nametab.global does not work with variables and *)
 (*CSC: we have to do this hugly try ... with                        *)
    try
-    Nt.global locqid
+    Nt.global r
    with
-    _ -> let (_,id) = Ln.repr_qualid qid in Ln.VarRef id
+    _ ->
+      let (_,id) = Ln.repr_qualid (snd (Ln.qualid_of_reference r)) in
+      Ln.VarRef id
   in
   (* Variables are the identifiers of the variables in scope *)
   let variables = search_variables () in
@@ -761,14 +763,17 @@ let filename_of_path ?(keep_sections=false) xml_library_root kn tag =
 ;;
 
 (*CSC: Ask Hugo for a better solution *)
-let qualid_of_kernel_name kn =
+(*
+let ref_of_kernel_name kn =
  let module N = Names in
+ let module Ln = Libnames in
   let (modpath,_,label) = N.repr_kn kn in
    match modpath with
-      N.MPself _ -> Libnames.make_qualid (Lib.cwd ()) (N.id_of_label label)
+      N.MPself _ -> Ln.Qualid (Ln.qualid_of_sp (Nametab.sp_of_global None kn))
     | _ ->
-      Util.anomaly ("qualid_of_kernel_name: the module path is not MPself")
+      Util.anomaly ("ref_of_kernel_name: the module path is not MPself")
 ;;
+*)
 
 (* Let's register the callbacks *)
 let xml_library_root =
@@ -787,37 +792,37 @@ let _ =
 
 let _ =
   Declare.set_xml_declare_variable
-   (function kn ->
+   (function (sp,kn) ->
      let filename =
       filename_of_path ~keep_sections:true xml_library_root kn
        Cic2acic.Variable in
-     let qualid = qualid_of_kernel_name kn in
      let dummy_location = -1,-1 in
-      print (dummy_location,qualid) filename)
+     let ref = Libnames.Qualid (dummy_location,Libnames.qualid_of_sp sp) in
+      print ref filename)
 ;;
 
 let _ =
   Declare.set_xml_declare_constant
-   (function kn ->
+   (function (sp,kn) ->
      let filename = filename_of_path xml_library_root kn Cic2acic.Constant in
-     let qualid = qualid_of_kernel_name kn in
+     let dummy_location = -1,-1 in
+     let ref = Libnames.Qualid (dummy_location,Libnames.qualid_of_sp sp) in
      match !proof_to_export with
         None ->
-         let dummy_location = -1,-1 in
-          print (dummy_location,qualid) filename
+          print ref filename
       | Some pftreestate ->
          (* It is a proof. Let's export it starting from the proof-tree *)
          (* I saved in the Pfedit.set_xml_cook_proof callback.          *)
-         show_pftreestate filename pftreestate
-          (Names.id_of_label (Names.label kn)) ;
+         show_pftreestate filename pftreestate 
+	  (Names.id_of_label (Names.label kn)) ;
          proof_to_export := None)
 ;;
 
 let _ =
   Declare.set_xml_declare_inductive
-   (function kn ->
+   (function (sp,kn) ->
      let filename = filename_of_path xml_library_root kn Cic2acic.Inductive in
-     let qualid = qualid_of_kernel_name kn in
      let dummy_location = -1,-1 in
-      print (dummy_location,qualid) filename)
+     let ref = Libnames.Qualid (dummy_location,Libnames.qualid_of_sp sp) in
+      print ref filename)
 ;;
diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli
index 4690e21c19..6e43be9c20 100644
--- a/contrib/xml/xmlcommand.mli
+++ b/contrib/xml/xmlcommand.mli
@@ -28,7 +28,7 @@
 (* Note: it is printed only (and directly) the most cooked available      *)
 (*       form of the definition (all the parameters are                   *)
 (*       lambda-abstracted, but the object can still refer to variables)  *)
-val print : Libnames.qualid Util.located -> string option -> unit
+val print : Libnames.reference -> string option -> unit
 
 (* show dest                                                  *)
 (*  where dest is either None (for stdout) or (Some filename) *)
diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4
index fbb9944d37..6988f789ee 100644
--- a/contrib/xml/xmlentries.ml4
+++ b/contrib/xml/xmlentries.ml4
@@ -81,14 +81,14 @@ let _ =
     (wit_diskname, pr_diskname)
 
 VERNAC COMMAND EXTEND Xml
-| [ "Print" "XML" filename(fn) qualid(id) ] -> [ Xmlcommand.print id fn ]
+| [ "Print" "XML" filename(fn) global(id) ] -> [ Xmlcommand.print id fn ]
 
 | [ "Show" "XML" filename(fn) "Proof" ] -> [ Xmlcommand.show fn ]
 
 (*
 | [ "Print" "XML" "All" ] -> [ Xmlcommand.printAll () ]
 
-| [ "Print" "XML" "Module" diskname(dn) qualid(id) ] ->
+| [ "Print" "XML" "Module" diskname(dn) global(id) ] ->
     [ Xmlcommand.printLibrary id dn ]
 
 | [ "Print" "XML" "Section" diskname(dn) ident(id) ] ->