Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tactiques d'appliquer une éventuelle coercion vers le but

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

1 files changed, 3 insertions, 3 deletions

diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 081d7aeecc..496b6594d0 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 castedopenconstr = 
-      make_gen_entry utactic rawwit_casted_open_constr "castedopenconstr"
+    let openconstr = 
+      make_gen_entry utactic rawwit_open_constr "openconstr"
     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.castedopenconstr;
+  f Tactic.openconstr;
   f Tactic.constr_with_bindings;
   f Tactic.bindings;
   f Tactic.constrarg;