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/lib.ml b/library/lib.ml
index 323ca60de6..243fc1acaa 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -471,12 +471,12 @@ let reset_to sp =
   let (after,_,_) = split_lib spf in
   recache_context after
 
-let reset_name id =
+let reset_name (loc,id) =
   let (sp,_) = 
     try
       find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi)
     with Not_found ->
-      error (string_of_id id ^ ": no such entry")
+      user_err_loc (loc,"reset_name",pr_id id ++ str ": no such entry")
   in
   reset_to sp