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, 2 insertions, 2 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index 4d505b5aa..4c2d15206 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -177,7 +177,7 @@ let get_ref_table k = List.assoc (nickname k) !ref_table
 module type RefConvertArg =
 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
@@ -189,7 +189,7 @@ end
 module RefConvert = functor (A : RefConvertArg) -> 
 struct
   type t = A.t
-  type key = qualid located
+  type key = reference
   let table = ref_table
   let encode = A.encode
   let subst = A.subst