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

3 files changed, 14 insertions, 14 deletions

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