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

13 files changed, 176 insertions, 138 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 4c57760de..d5715fd3d 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 b917f24d4..3a4806924 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 2345ff471..17bd6ef4e 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 3be5d8a36..00a4bb07e 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 dc2b2734c..f556c1926 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 b4db22803..343f90d6e 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 ec600d21d..a7e1f3444 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 600ec5f91..0eca0a1e7 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 61fd06072..a8d74c30e 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 7bd29a958..469a067f4 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 c7e6be131..4ae1f280d 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 c84642d77..ee2694585 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 92a35b892..a5a153bdb 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