Parsing

- 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@1889 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 28 insertions, 17 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 8cbfcc0a5b..556dbd3341 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -14,6 +14,7 @@ open Options
 open Names
 open Environ
 open Libobject
+open Library
 open Declare
 open Term
 open Rawterm
@@ -30,7 +31,7 @@ let cte_of_constr c = match kind_of_term c with
   | IsConst (sp,_) -> ConstRef sp
   | IsMutInd (ind_sp,_) -> IndRef ind_sp
   | IsMutConstruct (cstr_cp,_) -> ConstructRef cstr_cp
-  | IsVar id -> VarRef (find_section_variable id)
+  | IsVar id -> VarRef (Declare.find_section_variable id)
   |  _ -> raise Not_found
 
 type cl_typ = 
diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml
index 6a171d7c46..1b875affa7 100644
--- a/pretyping/syntax_def.ml
+++ b/pretyping/syntax_def.ml
@@ -8,6 +8,8 @@
 
 (* $Id$ *)
 
+open Util
+open Pp
 open Names
 open Rawterm
 open Libobject
@@ -27,31 +29,39 @@ let _ = Summary.declare_summary
 let add_syntax_constant sp c =
   syntax_table := Spmap.add sp c !syntax_table
 
-(* Impossible de rendre récursive la définition de in_syntax_constant
-   et cache_syntax_constant, alors on triche ... *)
-let cache_syntax_constant = ref (fun c -> failwith "Undefined function")
+let cache_syntax_constant (sp,c) =
+  if Nametab.exists_cci sp then
+    errorlabstrm "cache_syntax_constant"
+      [< pr_id (basename sp); 'sTR " already exists" >];
+  add_syntax_constant sp c;
+  Nametab.push_syntactic_definition sp;
+  Nametab.push_short_name_syntactic_definition sp
+
+let load_syntax_constant (sp,c) =
+  if Nametab.exists_cci sp then
+    errorlabstrm "cache_syntax_constant"
+      [< pr_id (basename sp); 'sTR " already exists" >];
+  add_syntax_constant sp c;
+  Nametab.push_syntactic_definition sp
+
+let open_syntax_constant (sp,c) =
+  Nametab.push_short_name_syntactic_definition sp
 
 let (in_syntax_constant, out_syntax_constant) =
   let od = {
-    cache_function = (fun c -> !cache_syntax_constant c);
-    load_function = (fun _ -> ());
-    open_function = (fun c -> !cache_syntax_constant c);
+    cache_function = cache_syntax_constant;
+    load_function = load_syntax_constant;
+    open_function = open_syntax_constant;
     export_function = (fun x -> Some x) } 
   in
   declare_object ("SYNTAXCONSTANT", od)
 
-let _ =
-  cache_syntax_constant := fun (sp,c) ->
-    add_syntax_constant sp c;
-    Nametab.push_object sp (in_syntax_constant c)
-
 let declare_syntactic_definition id c =
   let _ = add_leaf id CCI (in_syntax_constant c) in ()
 
 let search_syntactic_definition sp = Spmap.find sp !syntax_table
 
-let locate_syntactic_definition sp =
-  let (sp,obj) = Nametab.locate_obj sp in
-  if object_tag obj = "SYNTAXCONSTANT" then sp else raise Not_found
-  
-
+let locate_syntactic_definition qid =
+  match Nametab.extended_locate qid with
+    | Nametab.SyntacticDef sp -> sp
+    | _ -> raise Not_found