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

1 files changed, 9 insertions, 9 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index dd35bc58f4..613c0a475c 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -39,7 +39,7 @@ type morphism =
 let constr_of c = Astterm.interp_constr Evd.empty (Global.env()) c
 
 let constant dir s =
-  let dir = "Coq"::"Setoid"::dir in
+  let dir = make_dirpath (List.map id_of_string ("Coq"::"Setoid"::dir)) in
   let id = id_of_string s in
     try 
       Declare.global_reference_in_absolute_module dir id
@@ -47,7 +47,7 @@ let constant dir s =
     anomaly ("Setoid: cannot find "^(Nametab.string_of_qualid (Nametab.make_qualid dir id)))
 
 let global_constant dir s =
-  let dir = "Coq"::"Init"::dir in
+  let dir = make_dirpath (List.map id_of_string ("Coq"::"Init"::dir)) in
   let id = id_of_string s in
     try 
       Declare.global_reference_in_absolute_module dir id
@@ -206,7 +206,7 @@ let gen_eq_lem_name =
   let i = ref 0 in
     function () -> 
       incr i;
-      id_of_string ("setoid_eq_ext"^(string_of_int !i))
+      make_ident "setoid_eq_ext" (Some !i)
 
 let add_setoid a aeq th =
   if setoid_table_mem a 
@@ -289,11 +289,11 @@ let check_is_dependent t n =
   in aux t 0 n
 
 let gen_lem_name m = match kind_of_term m with 
-  | IsVar id -> id_of_string ((string_of_id id)^"_ext")
-  | IsConst (sp, _) -> id_of_string ((string_of_id(basename sp))^"_ext")
-  | IsMutInd ((sp, i), _) -> id_of_string ((string_of_id(basename sp))^(string_of_int i)^"_ext")
-  | IsMutConstruct (((sp,i),j), _) -> id_of_string 
-      ((string_of_id(basename sp))^(string_of_int i)^(string_of_int i)^"_ext")
+  | IsVar id -> add_suffix id "_ext"
+  | IsConst (sp, _) -> add_suffix (basename sp) "_ext"
+  | IsMutInd ((sp, i), _) -> add_suffix (basename sp) ((string_of_int i)^"_ext")
+  | IsMutConstruct (((sp,i),j), _) -> add_suffix
+      (basename sp) ((string_of_int i)^(string_of_int i)^"_ext")
   | _ -> errorlabstrm "New Morphism" [< 'sTR "The term "; prterm m; 'sTR "is not a known name">]
 
 let gen_lemma_tail m lisset body n =
@@ -449,7 +449,7 @@ let add_morphism lem_name (m,profil) =
       (if (eq_constr body mkProp)
        then
 	 (let lem_2 = gen_lem_iff env m mext args_t poss in
-	  let lem2_name = (id_of_string ((string_of_id lem_name)^"2")) in
+	  let lem2_name = add_suffix lem_name "2" in
 	  let _ = Declare.declare_constant lem2_name
 		    ((Declare.ConstantEntry {Declarations.const_entry_body = lem_2; 
 					     Declarations.const_entry_type = None}),