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

8 files changed, 32 insertions, 32 deletions

diff --git a/tactics/Inv.v b/tactics/Inv.v
index 39a434b01..2b9271aca 100644
--- a/tactics/Inv.v
+++ b/tactics/Inv.v
@@ -49,7 +49,7 @@ Grammar tactic simple_tactic: ast :=
 
 | inv_using [ inversion_com($ic) identarg($id) "using" constrarg($c) ]
      -> case [$ic] of
-          Inversion -> [(UseInversionLemma $id $c)]
+          "Inversion" -> [(UseInversionLemma $id $c)]
         esac
 
 | inv_num_using [ inversion_com($ic) pure_numarg($n) "using" constrarg($c) ]
@@ -61,13 +61,13 @@ Grammar tactic simple_tactic: ast :=
    [ inversion_com($ic) identarg($id) "using" constrarg($c)
      "in" ne_identarg_list($l) ]
      -> case [$ic] of
-          Inversion -> [(UseInversionLemmaIn $id $c ($LIST $l))]
+          "Inversion" -> [(UseInversionLemmaIn $id $c ($LIST $l))]
         esac
 
 with inversion_com: ast :=
-  simple_inv    [ "Simple" "Inversion" ] -> [ HalfInversion ]
-| inversion_com [ "Inversion" ] -> [ Inversion ]
-| inv_clear     [ "Inversion_clear" ] -> [ InversionClear ].
+  simple_inv    [ "Simple" "Inversion" ] -> [ "HalfInversion" ]
+| inversion_com [ "Inversion" ] -> [ "Inversion" ]
+| inv_clear     [ "Inversion_clear" ] -> [ "InversionClear" ].
 
 
 Grammar vernac vernac: ast :=
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 211ecbf6d..839c63978 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -253,8 +253,8 @@ let match_dpat dp cls gls =
 let applyDestructor cls discard dd gls =
   let mvb = match_dpat dd.d_pat cls gls in
   let astb = match cls with
-    | Some id -> ["$0", Vast (nvar (string_of_id id))]
-    | None -> ["$0", Vast (nvar "$0")] in
+    | Some id -> ["$0", Vast (nvar id)]
+    | None -> ["$0", Vast (nvar (id_of_string "$0"))] in
   (* TODO: find the real location *)
   let tcom = match Ast.eval_act dummy_loc astb dd.d_code with
     | Vast tcom -> tcom
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 4e0c39ab2..3fbe8e8ee 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -413,9 +413,9 @@ let inv gene com status id =
   in 
   fun gls -> try tac gls with e -> wrap_inv_error id e
 
-let hinv_kind = Identifier (id_of_string "HalfInversion")
-let inv_kind = Identifier (id_of_string "Inversion")
-let invclr_kind = Identifier (id_of_string "InversionClear")
+let hinv_kind = Quoted_string "HalfInversion"
+let inv_kind = Quoted_string "Inversion"
+let invclr_kind = Quoted_string "InversionClear"
 
 let com_of_id id =
   if id = hinv_kind then None
@@ -519,6 +519,6 @@ let invIn_tac =
   in 
   fun com id hl ->
     gentac
-      ((Identifier (id_of_string com))
+      ((Identifier com)
        ::(Identifier id)
        ::(List.map (fun id -> (Identifier id)) hl))
diff --git a/tactics/inv.mli b/tactics/inv.mli
index ed0dc1de0..792f13261 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -24,4 +24,4 @@ val half_dinv_with : identifier -> constr -> tactic
 val dinv_with : identifier -> constr -> tactic
 val dinv_clear_with : identifier -> constr -> tactic
 
-val invIn_tac : string -> identifier -> identifier list -> tactic
+val invIn_tac : identifier -> identifier -> identifier list -> tactic
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index dd35bc58f..613c0a475 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}),
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index cb8644383..9d8f07d78 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -312,12 +312,6 @@ let last_arg c = match kind_of_term c with
 let general_elim_then_using 
   elim elim_sign_fun tac predicate (indbindings,elimbindings) c gl =
   let ((ity,_,_),t) = reduce_to_ind_goal gl (pf_type_of gl c) in
-  let name_elim =
-    (match kind_of_term elim with
-       | IsConst (sp,_) -> id_of_string (string_of_path sp)
-       | IsVar id -> id
-       | _ -> id_of_string " ") 
-  in
   (* applying elimination_scheme just a little modified *)
   let (wc,kONT)  = startWalk gl in
   let indclause  = mk_clenv_from wc (c,t) in
@@ -332,8 +326,14 @@ let general_elim_then_using
     let p, _ = decomp_app (clenv_template_type elimclause).rebus in
     match kind_of_term p with
       | IsMeta p -> p
-      | _ -> error ("The elimination combinator " ^
-                    (string_of_id name_elim) ^ " is not known") 
+      | _ ->
+	  let name_elim =
+	    match kind_of_term elim with
+	      | IsConst (sp,_) -> string_of_path sp
+	      | IsVar id -> string_of_id id
+	      | _ -> "\b"
+	  in
+	  error ("The elimination combinator " ^ name_elim ^ " is not known") 
   in
   let elimclause' = clenv_fchain indmv elimclause indclause' in
   let elimclause' = clenv_constrain_with_bindings elimbindings elimclause' in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index bffbfea4c..12b41b602 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1823,7 +1823,7 @@ let abstract_subproof name tac gls =
   in
   if occur_existential concl then error "Abstract cannot handle existentials";
   let lemme =
-    start_proof na Declare.NeverDischarge current_sign concl;
+    start_proof na NeverDischarge current_sign concl;
     let _,(const,strength) =
       try
 	by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); 
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 7edf1610e..599644927 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -115,7 +115,7 @@ let rec intuition_main () =
 let unfold_not_iff = function
   | None -> interp <:tactic<Unfold not iff>>
   | Some id ->
-    let ast_id = nvar (string_of_id id) in
+    let ast_id = nvar id in
     interp <:tactic<Unfold not iff in $ast_id>>
 
 let reduction_not_iff = Tacticals.onAllClauses (fun ido -> unfold_not_iff ido)
@@ -123,7 +123,7 @@ let reduction_not_iff = Tacticals.onAllClauses (fun ido -> unfold_not_iff ido)
 let compute = function
   | None -> interp <:tactic<Compute>>
   | Some id ->
-    let ast_id = nvar (string_of_id id) in
+    let ast_id = nvar id in
     interp <:tactic<Compute in $ast_id>>
 
 let reduction = Tacticals.onAllClauses (fun ido -> compute ido)