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

3 files changed, 8 insertions, 11 deletions

diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index ecc17253a..d13be7720 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -48,7 +48,7 @@ let tuple_n n =
       (fun i -> 
 	 let id = id_of_string 
 		    ("proj_" ^ string_of_int n ^ "_" ^ string_of_int i) in
-	 (false, (id, true, Ast.nvar ("T" ^ string_of_int i))))
+	 (false, (id, true, Ast.nvar (id_of_string ("T" ^ string_of_int i)))))
       l1n 
   in
   let cons = id_of_string ("Build_tuple_" ^ string_of_int n) in
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index d6a15959b..c885242bd 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -120,23 +120,19 @@ let subst_in_constr alist =
   replace_vars alist'
 
 let subst_in_ast alist ast =
-  let alist' = 
-    List.map (fun (id,id') -> (string_of_id id,string_of_id id')) alist in
   let rec subst = function
-      Nvar(l,s) -> Nvar(l,try List.assoc s alist' with Not_found -> s)
+      Nvar(l,s) -> Nvar(l,try List.assoc s alist with Not_found -> s)
     | Node(l,s,args) -> Node(l,s,List.map subst args)
-    | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist' ? *)
+    | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist ? *)
     | x -> x
   in
     subst ast
 
 let subst_ast_in_ast alist ast =
-  let alist' = 
-    List.map (fun (id,a) -> (string_of_id id,a)) alist in
   let rec subst = function
-      Nvar(l,s) as x -> (try List.assoc s alist' with Not_found -> x)
+      Nvar(l,s) as x -> (try List.assoc s alist with Not_found -> x)
     | Node(l,s,args) -> Node(l,s,List.map subst args)
-    | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist' ? *)
+    | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist ? *)
     | x -> x
   in
     subst ast
@@ -146,7 +142,8 @@ let real_subst_in_constr = replace_vars
 
 (* Coq constants *)
 
-let coq_constant d s = make_path ("Coq" :: d) (id_of_string s) CCI
+let coq_constant d s =
+  make_path (List.map id_of_string ("Coq" :: d)) (id_of_string s) CCI
 
 let bool_sp = coq_constant ["Init"; "Datatypes"] "bool"
 let coq_true = mkMutConstruct (((bool_sp,0),1), [||])
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 5e0f9ad42..fc09cfa69 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -561,7 +561,7 @@ open Vernac
 GEXTEND Gram
   Pcoq.Vernac_.vernac:
   [ [ IDENT "Global"; "Variable"; 
-      l = LIST1 IDENT SEP ","; ":"; t = type_v; "." ->
+      l = LIST1 ident SEP ","; ":"; t = type_v; "." ->
 	let idl = List.map Ast.nvar l in
 	let d = Ast.dynamic (in_typev t) in
 	  <:ast< (PROGVARIABLE (VERNACARGLIST ($LIST $idl)) (VERNACDYN $d)) >>