Prsing

- Typage renforcé dans les grammaires (distinction des vars et des metavars)
- Disparition de SLAM au profit de ABSTRACT
- Paths primitifs dans les quotations (syntaxe concrète à base de .)
- Mise en place de identifier dès le type ast
- Protection de identifier contre les effets de bord via un String.copy
- Utilisation de module_ident (= identifier) dans les dir_path (au
  lieu de string)

Table des noms qualifiés

- Remplacement de la table de visibilité par une table qui ne cache
  plus les noms de modules et sections mais seulement les noms des
  constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel
  module A déjà existant : seuls les noms de constructions de l'ancien
  A qui existent aussi dans le nouveau A seront cachés)
- Renoncement à la possibilité d'accéder les formes non déchargées des
  constantes définies à l'intérieur de sections et simplification
  connexes (suppression de END-SECTION, une seule table de noms qui ne
  survit pas au discharge)
- Utilisation de noms longs pour les modules, de noms qualifiés pour
  Require and co, tests de cohérence; pour être cohérent avec la non
  survie des tables de noms à la sortie des section, les require à
  l'intérieur d'une section eux aussi sont refaits à la fermeture de la
  section


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

13 files changed, 155 insertions, 80 deletions

diff --git a/contrib/interface/Centaur.v b/contrib/interface/Centaur.v
index f2e168645..5cca616a5 100644
--- a/contrib/interface/Centaur.v
+++ b/contrib/interface/Centaur.v
@@ -1,3 +1,4 @@
+Declare ML Module "ctast".
 Declare ML Module "paths".
 Declare ML Module "name_to_ast".
 Declare ML Module "xlate".
@@ -73,10 +74,10 @@ Grammar tactic simple_tactic : ast :=
    procedure changed from V6.1 and does not reprint the command anymore. *)
 Grammar vernac vernac : ast :=
   text_proof_flag_on [ "Text" "Mode" "fr" "." ] ->
-       [(TEXT_MODE (AST {fr}))]
+       [(TEXT_MODE (AST "fr"))]
 | text_proof_flag_on [ "Text" "Mode" "en" "." ] ->
-       [(TEXT_MODE (AST {en}))]
+       [(TEXT_MODE (AST "en"))]
 | text_proof_flag_on [ "Text" "Mode" "Off" "." ] ->
-       [(TEXT_MODE (AST {off}))].
+       [(TEXT_MODE (AST "off"))].
 
 
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index d6eaf0c6d..3dff01937 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -1,3 +1,4 @@
+
 type ct_ASSOC =
     CT_coerce_NONE_to_ASSOC of ct_NONE
   | CT_lefta
diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml
index 6e1555d59..e4c852f7f 100644
--- a/contrib/interface/centaur.ml
+++ b/contrib/interface/centaur.ml
@@ -302,12 +302,12 @@ and ntyp = nf_betaiota typ in
 
 (* The following function is copied from globpr in env/printer.ml *)
 let globcv = function
-  | Node(_,"MUTIND", (Path(_,sl,s))::(Num(_,tyi))::_) ->
+  | Node(_,"MUTIND", (Path(_,sp))::(Num(_,tyi))::_) ->
        convert_qualid
-	 (Global.qualid_of_global (IndRef(section_path sl s,tyi)))
-  | Node(_,"MUTCONSTRUCT",(Path(_,sl,s))::(Num(_,tyi))::(Num(_,i))::_) ->
+	 (Global.qualid_of_global (IndRef(sp,tyi)))
+  | Node(_,"MUTCONSTRUCT",(Path(_,sp))::(Num(_,tyi))::(Num(_,i))::_) ->
        convert_qualid
-          (Global.qualid_of_global (ConstructRef ((section_path sl s, tyi), i)))
+          (Global.qualid_of_global (ConstructRef ((sp, tyi), i)))
   | _ -> failwith "globcv : unexpected value";;
 
 let pbp_tac_pcoq =
@@ -446,7 +446,7 @@ let logical_kill n =
 let command_changes = [
   ("TEXT_MODE",
    (function
-     |  [VARG_AST (Id(_,x))] ->
+     |  [VARG_AST (Str(_,x))] ->
 	 (match x with
 	   "fr" -> (function () -> text_proof_flag := "fr")
 	 | "en" -> (function () -> text_proof_flag := "en")
@@ -626,7 +626,7 @@ let command_changes = [
    (function
       | [VARG_QUALID qid] ->
 	 (function () -> 
-	   let results = xlate_vernac_list (name_to_ast qid) in
+	   let results = xlate_vernac_list (Ctast.ast_to_ct (name_to_ast qid)) in
 	   output_results 
 	     [<'fNL; 'sTR "message"; 'fNL; 'sTR "PRINT_VALUE"; 'fNL >]
 	     (Some (P_cl results)))
@@ -653,7 +653,7 @@ let command_changes = [
      | VARG_TACTIC_ARG(Redexp redexp):: VARG_CONSTR c :: g ->
 	 let evmap, env = Vernacentries.get_current_context_of_args g in
 	 let redfun =
-	   ct_print_eval c (Tacred.reduction_of_redexp redexp env evmap) env in
+	   ct_print_eval (Ctast.ast_to_ct c) (Tacred.reduction_of_redexp redexp env evmap) env in
 	 fun () -> 
 	   let strm, vtp = redfun evmap (judgment_of_rawconstr evmap env c) in
 	   output_results strm vtp
@@ -728,7 +728,7 @@ let command_creations = [
 let start_pcoq_mode debug = 
   begin
     start_dad();
-    set_xlate_mut_stuff globcv;
+    set_xlate_mut_stuff (fun x ->Ctast.ast_to_ct (globcv (Ctast.ct_to_ast x)));
     declare_in_coq();
     add_tactic "PcoqPbp" pbp_tac_pcoq;
     add_tactic "Dad" dad_tac_pcoq;
diff --git a/contrib/interface/ctast.ml b/contrib/interface/ctast.ml
new file mode 100644
index 000000000..4ed6dbcd9
--- /dev/null
+++ b/contrib/interface/ctast.ml
@@ -0,0 +1,69 @@
+(* A copy of pre V7 ast *)
+
+open Names
+
+type loc = int * int
+
+type t =
+  | Node of loc * string * t list
+  | Nvar of loc * string
+  | Slam of loc * string option * t
+  | Num of loc * int
+  | Id of loc * string
+  | Str of loc * string
+  | Path of loc * string list* string
+  | Dynamic of loc * Dyn.t
+
+let section_path sl k =
+  match List.rev sl with
+    | s::pa -> make_path (List.rev (List.map id_of_string pa)) (id_of_string s) (kind_of_string k)
+    | [] -> invalid_arg "section_path"
+
+let is_meta s = String.length s > 0 && s.[0] == '$'
+
+let purge_str s =
+  if String.length s == 0 || s.[0] <> '$' then s
+  else String.sub s 1 (String.length s - 1)
+
+let rec ct_to_ast = function
+  | Node (loc,a,b) -> Coqast.Node (loc,a,List.map ct_to_ast b)
+  | Nvar (loc,a) ->
+      if is_meta a then Coqast.Nmeta (loc,purge_str a)
+      else Coqast.Nvar (loc,id_of_string a)
+  | Slam (loc,Some a,b) ->
+      if is_meta a then Coqast.Smetalam (loc,purge_str a,ct_to_ast b)
+      else Coqast.Slam (loc,Some (id_of_string a),ct_to_ast b)
+  | Slam (loc,None,b) -> Coqast.Slam (loc,None,ct_to_ast b)
+  | Num (loc,a) -> Coqast.Num (loc,a)
+  | Id (loc,a) -> Coqast.Id (loc,a)
+  | Str (loc,a) -> Coqast.Str (loc,a)
+  | Path (loc,sl,k) -> Coqast.Path (loc,section_path sl k)
+  | Dynamic (loc,a) -> Coqast.Dynamic (loc,a)
+
+let rec ast_to_ct = function
+  | 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)
+  | Coqast.Slam (loc,Some a,b) ->
+   Slam (loc,Some (string_of_id a),ast_to_ct b)
+  | Coqast.Slam (loc,None,b) -> Slam (loc,None,ast_to_ct b)
+  | Coqast.Smetalam (loc,a,b) -> Slam (loc,Some ("$"^a),ast_to_ct b)
+  | Coqast.Num (loc,a) -> Num (loc,a)
+  | Coqast.Id (loc,a) -> Id (loc,a)
+  | Coqast.Str (loc,a) -> Str (loc,a)
+  | Coqast.Path (loc,a) ->
+    let (sl,bn,pk) = repr_path a in
+    Path(loc, (List.map string_of_id sl) @ [string_of_id bn],(* Bidon *) "CCI")
+  | Coqast.Dynamic (loc,a) -> Dynamic (loc,a)
+
+let loc = function
+  | Node (loc,_,_) -> loc
+  | Nvar (loc,_) -> loc
+  | Slam (loc,_,_) -> loc
+  | Num (loc,_) -> loc
+  | Id (loc,_) -> loc
+  | Str (loc,_) -> loc
+  | Path (loc,_,_) -> loc
+  | Dynamic (loc,_) -> loc
+
+let str s = Str(Ast.dummy_loc,s)
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index c26a8039d..f84fe33ef 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -11,7 +11,7 @@ open Tactics;;
 open Tacticals;;
 open Pattern;;
 open Reduction;;
-open Coqast;;
+open Ctast;;
 open Termast;;
 open Astterm;;
 open Vernacinterp;;
@@ -36,10 +36,10 @@ open Paths;;
 *)
 
 
-type dad_rule = Coqast.t * int list * int list * int * int list * Coqast.t;;
+type dad_rule = Ctast.t * int list * int list * int * int list * Ctast.t;;
 
 (* This value will be used systematically when constructing objects of
-   type Coqast.t, the value is stupid and meaningless, but it is needed
+   type Ctast.t, the value is stupid and meaningless, but it is needed
    to construct well-typed terms. *)
 
 let zz = (0,0);;
@@ -66,7 +66,7 @@ let map_subst (env :env)
    let rec map_subst_aux = function
     Node(_, "META", [Num(_, i)]) ->
       let constr = List.assoc i subst in
-      ast_of_constr false env constr
+      Ctast.ast_to_ct (ast_of_constr false env constr)
   | Node(loc, s, l) -> Node(loc, s, List.map map_subst_aux l)
   | ast -> ast in
     map_subst_aux;;
@@ -89,7 +89,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())
-               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
            map_subst env subst cmd
@@ -251,7 +251,7 @@ vinterp_add "AddDadRule"
              VARG_NUMBERLIST p2; VARG_TACTIC com] ->
             (function () ->
               let pr = match decompose_path (p1, p2) with pr, _, _ -> pr in
-              (add_dad_rule name pat p1 p2 (List.length pr) pr com))
+              (add_dad_rule name (Ctast.ast_to_ct pat) p1 p2 (List.length pr) pr (Ctast.ast_to_ct com)))
             | _ -> errorlabstrm "AddDadRule1"
                     [< 'sTR "AddDadRule2">]);
 add_dad_rule "distributivity-inv"
diff --git a/contrib/interface/dad.mli b/contrib/interface/dad.mli
index 1d097804a..9f8f7354b 100644
--- a/contrib/interface/dad.mli
+++ b/contrib/interface/dad.mli
@@ -4,7 +4,7 @@ open Tacmach;;
 
 val dad_rule_names : unit -> string list;;
 val start_dad : unit -> unit;;
-val dad_tac : (Coqast.t -> 'a) -> tactic_arg list -> goal sigma ->
+val dad_tac : (Ctast.t -> 'a) -> tactic_arg list -> goal sigma ->
                   goal list sigma * validation;;
-val add_dad_rule : string -> Coqast.t -> (int list) -> (int list) ->
-                   int -> (int list) -> Coqast.t -> unit;;
+val add_dad_rule : string -> Ctast.t -> (int list) -> (int list) ->
+                   int -> (int list) -> Ctast.t -> unit;;
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 20122d576..6f1be02fb 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -26,7 +26,7 @@ let convert_env =
       match na with 
        | Name id ->
            ope("BINDER",
-               [ast_of_constr true env c;nvar(string_of_id id)])
+               [ast_of_constr true env c;nvar id])
        | Anonymous -> failwith "anomaly: Anonymous variables in inductives" in
     let rec cvrec env = function
        [] -> []
@@ -85,9 +85,9 @@ let implicit_args_to_ast_list sp mipv =
 let convert_qualid qid =
   let d, id = Nametab.repr_qualid qid in
     match d with
-	[] -> nvar(string_of_id id)
+	[] -> nvar id
       | _ -> ope("QUALID", List.fold_right (fun s l -> (nvar s)::l) d
-		   [nvar (string_of_id id)]);;
+		   [nvar id]);;
 
 (* This function converts constructors for an inductive definition to a
    Coqast.t.  It is obtained directly from print_constructors in pretty.ml *)
@@ -96,7 +96,7 @@ let convert_constructors envpar names types =
   let array_idC = 
     array_map2 
       (fun n t -> ope("BINDER",
-		      [ast_of_constr true envpar t; nvar(string_of_id n)]))
+		      [ast_of_constr true envpar t; nvar n]))
       names types in
     Node((0,0), "BINDERLIST", Array.to_list array_idC);;
   
@@ -163,9 +163,9 @@ let constant_to_ast_list sp =
       let l = constant_implicits_list sp in
 	(match c with
 	     None -> 
-	       make_variable_ast (string_of_id (basename sp)) typ l
+	       make_variable_ast (basename sp) typ l
 	   | Some c1 ->
-	       make_definition_ast (string_of_id (basename sp)) c1 typ l)
+	       make_definition_ast (basename sp) c1 typ l)
     else
       errorlabstrm "print" [< 'sTR "printing of FW terms not implemented" >];;
 
@@ -174,9 +174,9 @@ let variable_to_ast_list sp =
   let l = implicits_of_var sp in
     (match c with
 	 None -> 
-	   make_variable_ast (string_of_id id) v l
+	   make_variable_ast id v l
        | Some c1 ->
-	   make_definition_ast (string_of_id id) c1 v l);;
+	   make_definition_ast id c1 v l);;
 
 (* this function is taken from print_inductive in file pretty.ml *)
 
@@ -208,7 +208,7 @@ let leaf_entry_to_ast_list (sp,lobj) =
 let name_to_ast (qid:Nametab.qualid) = 
   let l = 
     try
-      let sp,_ = Nametab.locate_obj qid in
+      let sp = Nametab.locate_obj qid in
       let (sp,lobj) = 
       	let (sp,entry) =
           List.find (fun en -> (fst en) = sp) (Lib.contents_after None)
@@ -231,9 +231,8 @@ let name_to_ast (qid:Nametab.qualid) =
 	      if dir <> [] then raise Not_found;
 	      let (c,typ) = Global.lookup_named name in 
 		(match c with
-		     None -> make_variable_ast (string_of_id name) typ []
-		   | Some c1 -> make_definition_ast 
-		       (string_of_id name) c1 typ [])
+		     None -> make_variable_ast name typ []
+		   | Some c1 -> make_definition_ast name c1 typ [])
 	  with Not_found ->
 	    try
 	      let sp = Syntax_def.locate_syntactic_definition qid in
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index bdda47e38..ff76f2c75 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -4,7 +4,7 @@ open System;;
 
 open Pp;;
 
-open Coqast;;
+open Ctast;;
 
 open Library;;
 
@@ -58,14 +58,14 @@ let ctf_FileErrorMessage reqid pps =
   function has no effect on parsing *)
 let try_require_module import specif name fname =
  try Library.require_module (if specif = "UNSPECIFIED" then None
-  else Some (specif = "SPECIFICATION")) name fname (import = "IMPORT")
+  else Some (specif = "SPECIFICATION")) (Nametab.make_qualid [] (Names.id_of_string name)) fname (import = "IMPORT")
  with
  | e -> mSGNL [< 'sTR "Reinterning of "; 'sTR name; 'sTR " failed" >];;
 
 let execute_when_necessary ast =
  (match ast with
   | Node (_, "GRAMMAR", ((Nvar (_, s)) :: ((Node (_, "ASTLIST", al)) :: []))) ->
-   Metasyntax.add_grammar_obj s al
+   Metasyntax.add_grammar_obj s (List.map Ctast.ct_to_ast al)
   | Node (_, "TOKEN", ((Str (_, s)) :: [])) -> Metasyntax.add_token_obj s
   | Node (_, "Require",
             ((Str (_, import)) ::
@@ -91,9 +91,9 @@ let rec discard_to_dot stream =
 
 let rec decompose_string s n =
     try let index = String.index_from s n '\n' in
-            (Ast.str (String.sub s n (index - n)))::
+            (Ctast.str (String.sub s n (index - n)))::
             (decompose_string s (index + 1))
-    with Not_found -> [Ast.str(String.sub s n ((String.length s) - n))];;
+    with Not_found -> [Ctast.str(String.sub s n ((String.length s) - n))];;
 
 let make_string_list file_chan fst_pos snd_pos =
     let len = (snd_pos - fst_pos) in
@@ -140,11 +140,12 @@ let rec get_substring_list string_list fst_pos snd_pos =
 
 (* When parsing a list of commands, we try to recover error messages for
    each individual command. *)
+
 let parse_command_list reqid stream string_list =
     let rec parse_whole_stream () =
     let this_pos = Stream.count stream in
     let first_ast = 
-        try Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream)
+        try option_app Ctast.ast_to_ct (Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream))
         with
         | (Stdpp.Exc_located(l, Stream.Error txt)) as e -> 
           begin
@@ -154,7 +155,7 @@ let parse_command_list reqid stream string_list =
                 mSGNL [< 'sTR "debug"; 'fNL; 'iNT this_pos; 'fNL; 'iNT 
                   (Stream.count stream) >];
                 Some( Node(l, "PARSING_ERROR",
-                        List.map Ast.str
+                        List.map Ctast.str
                         (get_substring_list string_list this_pos
                             (Stream.count stream))))
              with End_of_file -> None
@@ -163,7 +164,7 @@ let parse_command_list reqid stream string_list =
           begin
             discard_to_dot stream;
             Some(Node((0,0), "PARSING_ERROR2",
-                   List.map Ast.str
+                   List.map Ctast.str
 		   (get_substring_list string_list this_pos
                      (Stream.count stream))))
           end in
@@ -190,25 +191,25 @@ let parse_string_action reqid phylum char_stream string_list =
        P_c
         (xlate_vernac
         (execute_when_necessary
-        (Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream))))
+        (Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream)))))
       | "TACTIC_COM" ->
        P_t
-        (xlate_tactic (Gram.Entry.parse Pcoq.Tactic.tactic_eoi 
-                         (Gram.parsable char_stream)))
+        (xlate_tactic (Ctast.ast_to_ct(Gram.Entry.parse Pcoq.Tactic.tactic_eoi 
+                         (Gram.parsable char_stream))))
       | "FORMULA" ->
        P_f
         (xlate_formula
-        (Gram.Entry.parse Pcoq.Constr.constr_eoi (Gram.parsable char_stream)))
+        (Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Constr.constr_eoi (Gram.parsable char_stream))))
       | "ID" -> P_id (xlate_id 
-                       (Gram.Entry.parse Pcoq.Prim.ident 
-                              (Gram.parsable char_stream)))
+                       (Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Prim.ident 
+                              (Gram.parsable char_stream))))
       | "STRING" ->
 	  P_s
-         (xlate_string (Gram.Entry.parse Pcoq.Prim.string 
-                  (Gram.parsable char_stream)))
+         (xlate_string (Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Prim.string 
+                  (Gram.parsable char_stream))))
       | "INT" ->
-	  P_i (xlate_int (Gram.Entry.parse Pcoq.Prim.number
-                              (Gram.parsable char_stream)))
+	  P_i (xlate_int (Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Prim.number
+                              (Gram.parsable char_stream))))
       | _ -> error "parse_string_action : bad phylum" in
       print_parse_results reqid msg
  with
@@ -242,7 +243,7 @@ let parse_file_action reqid file_name =
             match 
               try
                 let this_ast = 
-                     Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream) in
+                     option_app Ctast.ast_to_ct (Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream)) in
                 this_ast
               with
             | Stdpp.Exc_located(l,Stream.Error txt ) -> 
@@ -294,8 +295,7 @@ let add_path dir coq_dirpath =
   if coq_dirpath = [] then anomaly "add_path: empty path in library";
   if exists_dir dir then
     begin
-      Library.add_load_path_entry
-        { directory = dir; coq_dirpath = coq_dirpath };
+      Library.add_load_path_entry (dir,coq_dirpath);
       Nametab.push_library_root (List.hd coq_dirpath)
     end
   else
@@ -303,8 +303,10 @@ let add_path dir coq_dirpath =
 
 let add_rec_path dir coq_dirpath =
   if coq_dirpath = [] then anomaly "add_path: empty path in library";
-  let dirs = all_subdirs dir (Some coq_dirpath) in
+  let dirs = all_subdirs dir in
   if dirs <> [] then
+    let convert = List.map Names.id_of_string in
+    let dirs = List.map (fun (lp,cp) -> (lp,coq_dirpath@(convert cp))) dirs in
     begin
       List.iter Library.add_load_path_entry dirs;
       Nametab.push_library_root (List.hd coq_dirpath)
@@ -316,7 +318,7 @@ let add_path_action reqid string_arg =
   let directory_name = glob string_arg in
   let alias = Filename.basename directory_name in
     begin
-      add_path directory_name [alias]
+      add_path directory_name [Names.id_of_string alias]
     end;;
 
 let print_version_action () =
@@ -325,9 +327,12 @@ let print_version_action () =
 
 let load_syntax_action reqid module_name =
  mSG [< 'sTR "loading "; 'sTR module_name; 'sTR "... " >];
- try (load_module module_name None;
+ try
+      (let qid = Nametab.make_qualid [] (Names.id_of_string module_name) in
+      read_module qid;
       mSG [< 'sTR "opening... ">];
-      import_module module_name; 
+      let fullname = Nametab.locate_loaded_library qid in 
+      import_module fullname; 
       mSGNL [< 'sTR "done"; 'fNL >];
       ())
  with
@@ -367,7 +372,7 @@ Libobject.relax true;
        add_rec_path (Filename.concat coqdir "theories") [Nametab.coq_root];
        add_path (Filename.concat coqdir "tactics") [Nametab.coq_root];
        add_rec_path (Filename.concat coqdir "contrib") [Nametab.coq_root];
-       List.iter (fun {directory=a} -> mSGNL [< 'sTR a >]) (get_load_path())
+       List.iter (fun a -> mSGNL [< 'sTR a >]) (get_load_path())
      end;
 (try 
   (match create_entry (get_univ "nat") "number" ETast with
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index a5f44847b..409f5eb36 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -9,7 +9,7 @@ open Tacticals;;
 open Hipattern;;
 open Pattern;;
 open Reduction;;
-open Coqast;;
+open Ctast;;
 open Rawterm;;
 open Environ;;
 
@@ -38,8 +38,8 @@ type pbp_rule = (identifier list *
                     (identifier list ->
                      string list ->
                      bool ->
-                       string option -> (types, constr) kind_of_term -> int list -> Coqast.t)) ->
-                    Coqast.t option;;
+                       string option -> (types, constr) kind_of_term -> int list -> Ctast.t)) ->
+                    Ctast.t option;;
 
 let zz = (0,0);;
 
@@ -176,7 +176,7 @@ let (imply_elim2: pbp_rule) = function
   | _ -> None;;
 
 let reference dir s =
-  let dir = "Coq"::"Init"::[dir] in
+  let dir = List.map id_of_string ("Coq"::"Init"::[dir]) in
   let id = id_of_string s in
   try 
     Nametab.locate_in_absolute_module dir id
diff --git a/contrib/interface/pbp.mli b/contrib/interface/pbp.mli
index 649954019..57794ec22 100644
--- a/contrib/interface/pbp.mli
+++ b/contrib/interface/pbp.mli
@@ -1,4 +1,4 @@
-val pbp_tac : (Coqast.t -> 'a) ->
+val pbp_tac : (Ctast.t -> 'a) ->
     Proof_type.tactic_arg list ->
     Proof_type.goal Tacmach.sigma ->
     Proof_type.goal list Proof_type.sigma * Proof_type.validation;;
diff --git a/contrib/interface/translate.ml b/contrib/interface/translate.ml
index d40fee26a..75cd7db38 100644
--- a/contrib/interface/translate.ml
+++ b/contrib/interface/translate.ml
@@ -16,7 +16,7 @@ open Evd;;
 open Evarutil;;
 
 open Xlate;;
-open Coqast;;
+open Ctast;;
 open Vtp;;
 open Ascent;;
 open Environ;;
@@ -111,7 +111,7 @@ let rec discard_coercions =
 let translate_constr assumptions c =
  let com = ast_of_constr true assumptions c in
 (* dead code:  let rcom = relativize_cci (discard_coercions com) in *)
- xlate_formula com (* dead code: rcom *);;
+ xlate_formula (Ctast.ast_to_ct com) (* dead code: rcom *);;
 
 (*translates a named_context into a centaur-tree --> PREMISES_LIST *)
 (* this code is inspired from printer.ml (function pr_named_context_of) *)
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 63ef38e4f..ccaa08f50 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -6,14 +6,14 @@ open Char;;
 open Util;;
 open Ast;;
 open Names;;
+open Ctast;;
 open Ascent;;
-open Coqast;;
 
 let in_coq_ref = ref false;;
 
 let xlate_mut_stuff = ref ((fun _ -> 
           Nvar((0,0), "function xlate_mut_stuff should not be used here")):
-              Coqast.t -> Coqast.t);;
+              Ctast.t -> Ctast.t);;
 
 let set_xlate_mut_stuff v = xlate_mut_stuff := v;;
 
@@ -383,10 +383,10 @@ let xlate_op the_node opn a b =
   (match a, b with
   | ((Path (_, sl, kind)) :: []), [] ->
     CT_coerce_ID_to_FORMULA(CT_ident
-       (Names.string_of_id (Names.basename (Ast.section_path sl kind))))
+       (Names.string_of_id (Names.basename (section_path sl kind))))
   | ((Path (_, sl, kind)) :: []), tl ->
  CT_coerce_ID_to_FORMULA(CT_ident   
-       (Names.string_of_id(Names.basename (Ast.section_path sl kind))))
+       (Names.string_of_id(Names.basename (section_path sl kind))))
   | _, _ -> xlate_error "xlate_op : CONST")
  | (** string_of_path needs to be investigated.
     *)
@@ -402,7 +402,7 @@ let xlate_op the_node opn a b =
 	    CT_coerce_ID_to_FORMULA(
 	      CT_ident(Names.string_of_id
 			 (Names.basename
-			    (Ast.section_path sl kind))))
+			    (section_path sl kind))))
   	| _, _ -> xlate_error "xlate_op : MUTIND")
  | "MUTCASE" 
  | "CASE" ->
@@ -425,7 +425,7 @@ let xlate_op the_node opn a b =
 	 | Some(Rform x) -> x
 	 | _ -> assert false
    else
-   let name = Names.string_of_path (Ast.section_path sl kind) in
+   let name = Names.string_of_path (section_path sl kind) in
      (* This is rather a patch to cope with the fact that identifier
         names have disappeared from the vo files for grammar rules *)
        let type_desc = (try Some (Hashtbl.find type_table name) with
@@ -1372,7 +1372,7 @@ and xlate_tac =
      CT_user_tac (id, CT_targ_list (List.map coerce_iTARG_to_TARG l))
     | s, l ->
      CT_user_tac (CT_ident s, CT_targ_list (List.map coerce_iTARG_to_TARG l))
-and (xlate_context_rule: Coqast.t -> ct_CONTEXT_RULE) =
+and (xlate_context_rule: Ctast.t -> ct_CONTEXT_RULE) =
   function
     | Node(_, "MATCHCONTEXTRULE", parts) ->
 	let rec xlate_ctxt_rule_aux = function
diff --git a/contrib/interface/xlate.mli b/contrib/interface/xlate.mli
index 5613dd095..b93635e47 100644
--- a/contrib/interface/xlate.mli
+++ b/contrib/interface/xlate.mli
@@ -1,14 +1,14 @@
 open Ascent;;
 
-val xlate_vernac : Coqast.t -> ct_COMMAND;;
-val xlate_tactic : Coqast.t -> ct_TACTIC_COM;;
-val xlate_formula : Coqast.t -> ct_FORMULA;;
-val xlate_int : Coqast.t -> ct_INT;;
-val xlate_string : Coqast.t -> ct_STRING;;
-val xlate_id : Coqast.t -> ct_ID;;
-val xlate_vernac_list : Coqast.t -> ct_COMMAND_LIST;;
+val xlate_vernac : Ctast.t -> ct_COMMAND;;
+val xlate_tactic : Ctast.t -> ct_TACTIC_COM;;
+val xlate_formula : Ctast.t -> ct_FORMULA;;
+val xlate_int : Ctast.t -> ct_INT;;
+val xlate_string : Ctast.t -> ct_STRING;;
+val xlate_id : Ctast.t -> ct_ID;;
+val xlate_vernac_list : Ctast.t -> ct_COMMAND_LIST;;
 
 val g_nat_syntax_flag : bool ref;;
 val set_flags : (unit -> unit) ref;;
-val set_xlate_mut_stuff : (Coqast.t -> Coqast.t) -> unit;;
+val set_xlate_mut_stuff : (Ctast.t -> Ctast.t) -> unit;;
 val declare_in_coq : (unit -> unit);;