diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-06 11:28:22 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-06 11:28:22 +0000 |
| commit | f39cd683cb022d877a0d2ebd014fa0879bc6de00 (patch) | |
| tree | 1c691cb8f07513c905045b7b70d52872ed5e69dc /parsing/g_tacticnew.ml4 | |
| parent | c81e081287075310f78081728d4a6359f6ff017a (diff) | |
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
Diffstat (limited to 'parsing/g_tacticnew.ml4')
| -rw-r--r-- | parsing/g_tacticnew.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index 8930c8dca..70729ce13 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 castedopenconstr simple_intropattern; + bindings red_expr int_or_var openconstr simple_intropattern; int_or_var: [ [ n = integer -> Genarg.ArgArg n @@ -128,8 +128,8 @@ GEXTEND Gram | id = METAIDENT -> MetaId (loc,id) ] ] ; - castedopenconstr: - [ [ c = constr -> c ] ] + openconstr: + [ [ c = constr -> ((),c) ] ] ; induction_arg: [ [ n = natural -> ElimOnAnonHyp n |