Uniformisation du nom d'entrée openconstr en le nom du type open_constr

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

5 files changed, 9 insertions, 9 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 97f5d46a9d..b4e562706f 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -42,7 +42,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
 if !Options.v7 then
 GEXTEND Gram
   GLOBAL: simple_tactic constrarg bindings constr_with_bindings 
-  quantified_hypothesis red_expr int_or_var openconstr
+  quantified_hypothesis red_expr int_or_var open_constr
   simple_intropattern;
 
   int_or_var:
@@ -96,7 +96,7 @@ GEXTEND Gram
       | IDENT "Check"; c = constr -> ConstrTypeOf c
       | c = constr -> ConstrTerm c ] ]
   ;
-  openconstr:
+  open_constr:
     [ [ c = constr -> ((),c) ] ]
   ;
   induction_arg:
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 70729ce136..d869c5522c 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -109,7 +109,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
 if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
-  bindings red_expr int_or_var openconstr simple_intropattern;
+  bindings red_expr int_or_var open_constr simple_intropattern;
 
   int_or_var:
     [ [ n = integer  -> Genarg.ArgArg n
@@ -128,7 +128,7 @@ GEXTEND Gram
       |	id = METAIDENT -> MetaId (loc,id)
       ] ]
   ;
-  openconstr:
+  open_constr:
     [ [ c = constr -> ((),c) ] ]
   ;
   induction_arg:
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 496b6594d0..cc00806a5f 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -371,8 +371,8 @@ module Tactic =
 
     (* Entries that can be refered via the string -> Gram.Entry.e table *)
     (* Typically for tactic user extensions *)
-    let openconstr = 
-      make_gen_entry utactic rawwit_open_constr "openconstr"
+    let open_constr = 
+      make_gen_entry utactic rawwit_open_constr "open_constr"
     let constr_with_bindings =
       make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings"
     let bindings =
@@ -418,7 +418,7 @@ let reset_all_grammars () =
   f Constr.ident; f Constr.global; f Constr.sort; f Constr.pattern;
   f Module.module_expr; f Module.module_type;
   f Tactic.simple_tactic;
-  f Tactic.openconstr;
+  f Tactic.open_constr;
   f Tactic.constr_with_bindings;
   f Tactic.bindings;
   f Tactic.constrarg;
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 76c23ad20b..9c88106ee0 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -156,7 +156,7 @@ module Module :
 module Tactic :
   sig
     open Rawterm
-    val openconstr : open_constr_expr Gram.Entry.e
+    val open_constr : open_constr_expr Gram.Entry.e
     val constr_with_bindings : constr_expr with_bindings Gram.Entry.e
     val bindings : constr_expr bindings Gram.Entry.e
     val constrarg : (constr_expr,reference) may_eval Gram.Entry.e
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 4a68cbe9fc..b1ba9db486 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -159,7 +159,7 @@ END
 open Refine
 
 TACTIC EXTEND Refine
-  [ "Refine" openconstr(c) ] -> [ refine c ]
+  [ "Refine" open_constr(c) ] -> [ refine c ]
 END
 
 let refine_tac = h_refine