diff options
| author | herbelin | 2001-08-05 18:54:37 +0000 |
|---|---|---|
| committer | herbelin | 2001-08-05 18:54:37 +0000 |
| commit | 742cb1e14c773e9cc5ea5e1b35d361e4864943be (patch) | |
| tree | e1881468b3e6705366e7e28fc7b9b4f626bdcc99 /tactics/Inv.v | |
| parent | b6c60573dce9b6ad760c18b4853628c7da7c33e0 (diff) | |
Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'appliquer au but; appel optionnel de Intros Until sur certaines tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1878 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/Inv.v')
| -rw-r--r-- | tactics/Inv.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/Inv.v b/tactics/Inv.v index 36316ec811..12633311df 100644 --- a/tactics/Inv.v +++ b/tactics/Inv.v @@ -34,16 +34,16 @@ Syntax tactic level 0: Grammar tactic simple_tactic: ast := - inversion [ inversion_com($ic) identarg($id) ] -> [(Inv $ic $id)] + inversion [ inversion_com($ic) ident_or_numarg($id) ] -> [(Inv $ic $id)] | inversion_in [ inversion_com($ic) identarg($id) "in" ne_identarg_list($l) ] -> [(InvIn $ic $id ($LIST $l))] -| dep_inv [ "Dependent" inversion_com($ic) identarg($id) ] +| dep_inv [ "Dependent" inversion_com($ic) ident_or_numarg($id) ] -> [(DInv $ic $id)] | dep_inv_with - [ "Dependent" inversion_com($ic) identarg($id) "with" constrarg($c) ] + [ "Dependent" inversion_com($ic) ident_or_numarg($id) "with" constrarg($c) ] -> [(DInvWith $ic $id $c) ] -| inv_using [ inversion_com($ic) identarg($id) "using" constrarg($c) ] +| inv_using [ inversion_com($ic) ident_or_numarg($id) "using" constrarg($c) ] -> case [$ic] of Inversion -> [(UseInversionLemma $id $c)] esac |