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

1 files changed, 6 insertions, 6 deletions

diff --git a/library/goptions.mli b/library/goptions.mli
index 28da69ea6..f19d99aaa 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -94,8 +94,8 @@ sig
 end
 
 (* The functor [MakeRefTable] declares a new table of objects of type
-   [A.t] practically denoted by [qualid]; the encoding function
-   [encode : qualid -> A.t] is typically a globalization function,
+   [A.t] practically denoted by [reference]; the encoding function
+   [encode : reference -> A.t] is typically a globalization function,
    possibly with some restriction checks; the function
    [member_message] say what to print when invoking the "Test Toto
    Titi foo." command; at the end [title] is the table name printed
@@ -107,7 +107,7 @@ module MakeRefTable :
   functor
     (A : sig
            type t
-           val encode : qualid located -> t
+           val encode : reference -> t
 	   val subst : substitution -> t -> t
            val printer : t -> std_ppcmds
            val key : option_name
@@ -156,9 +156,9 @@ val get_string_table :
 
 val get_ref_table :
   option_name ->
-    < add : qualid located -> unit;
-      remove : qualid located -> unit;
-      mem : qualid located -> unit;
+    < add : reference -> unit;
+      remove : reference -> unit;
+      mem : reference -> unit;
       print : unit >
 
 val set_int_option_value    : option_name -> int option -> unit