renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocamldep

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1547 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 12 insertions, 12 deletions

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index cdfb55478a..4abce12f34 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -13,7 +13,7 @@
 open Coqast
 open Pcoq
 
-open Vernac
+open Vernac_
 
 GEXTEND Gram
   GLOBAL: identarg ne_identarg_list numarg ne_numarg_list numarg_list
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 05f4dc42ef..414c8eb0af 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -93,7 +93,7 @@ GEXTEND Gram
      | ":"; IDENT "tactic" ->
 	 let _ = set_default_action_parser Tactic.tactic in Id(loc,"AST")
      | ":"; IDENT "vernac" ->
-	 let _ = set_default_action_parser Vernac.vernac in Id(loc,"AST")
+	 let _ = set_default_action_parser Vernac_.vernac in Id(loc,"AST")
      | -> Id(loc,"AST") ]]
   ;
 END
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index efd6a5de21..6903293bbb 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -14,7 +14,7 @@ open Pcoq
 open Pp
 open Tactic
 open Util
-open Vernac
+open Vernac_
 
 (* Proof commands *)
 GEXTEND Gram
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index f26034c910..7aadc305d3 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -298,7 +298,7 @@ GEXTEND Gram
           <:ast< (StartProof "LETTOP" $id $c) >>
         | _ -> <:ast< (LETCUT (LETDECL ($LIST $llc))) >>)
       |	IDENT "Let"; llc = LIST1 let_clause SEP IDENT "And";
-        tb = Vernac.theorem_body; "Qed" ->
+        tb = Vernac_.theorem_body; "Qed" ->
         (match llc with
 	| [Coqast.Node(_,"LETTOPCLAUSE",[id;c])] ->
           <:ast< (TheoremProof "LETTOP" $id $c $tb) >>
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f1cae2458e..13a9ca9fb7 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -14,7 +14,7 @@ open Pcoq
 open Pp
 open Tactic
 open Util
-open Vernac
+open Vernac_
 
 (* Rem: do not join the different GEXTEND into one, it breaks native *)
 (* compilation on PowerPC and Sun architectures *)
@@ -280,7 +280,7 @@ GEXTEND Gram
       | bl = simple_binders -> bl ] ]
   ;
   rec_constr:
-    [ [ c = Vernac.identarg -> <:ast< (VERNACARGLIST $c) >>
+    [ [ c = Vernac_.identarg -> <:ast< (VERNACARGLIST $c) >>
       |  -> <:ast< (VERNACARGLIST) >> ] ]
   ;
   gallina_ext:
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 22fde95488..833f8a505e 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -338,7 +338,7 @@ module Tactic =
   end
 
 
-module Vernac =
+module Vernac_ =
   struct
     let uvernac = snd (get_univ "vernac")
     let gec s =
@@ -405,7 +405,7 @@ let main_entry = Gram.Entry.create "vernac"
 
 GEXTEND Gram
   main_entry:
-    [ [ a = Vernac.vernac -> Some a | EOI -> None ] ]
+    [ [ a = Vernac_.vernac -> Some a | EOI -> None ] ]
   ;
 END
 
@@ -414,7 +414,7 @@ END
 open Prim
 open Constr
 open Tactic
-open Vernac
+open Vernac_
 
 (* current file and toplevel/vernac.ml *)
 
@@ -446,7 +446,7 @@ let _ = define_quotation false "ast" ast in ()
 
 let constr_parser = ref Constr.constr
 let tactic_parser = ref Tactic.tactic
-let vernac_parser = ref Vernac.vernac
+let vernac_parser = ref Vernac_.vernac
 
 let update_constr_parser p = constr_parser := p
 let update_tactic_parser p = tactic_parser := p
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e640888625..7044801fa9 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -159,7 +159,7 @@ module Tactic :
     val with_binding_list : Coqast.t Gram.Entry.e
   end
 
-module Vernac :
+module Vernac_ :
   sig
     val identarg : Coqast.t Gram.Entry.e
     val ne_identarg_list : Coqast.t list Gram.Entry.e
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 0b6e92a43f..e8ee0c67d0 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -124,7 +124,7 @@ let f e =
 let _ = 
   Quotation.add "constr" (f Pcoq.Constr.constr_eoi);
   Quotation.add "tactic" (f Pcoq.Tactic.tactic_eoi);
-  Quotation.add "vernac" (f Pcoq.Vernac.vernac_eoi);
+  Quotation.add "vernac" (f Pcoq.Vernac_.vernac_eoi);
   Quotation.add "ast" (f Pcoq.Prim.ast_eoi);
   Quotation.default := "constr"