diff options
| author |  clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-03 10:02:45 +0000 |
|---|---|---|
| committer | clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-03 10:02:45 +0000 |
| commit | 6651f223752c9dfbe768273a09a7a4e67c2a5bfd (patch) | |
| tree | ee60b99811c0d7d5660fe9db1be86a61be725a42 | |
| parent | 8594c30c6d492aea98f99947feb9ed9b325ecc19 (diff) | |
Correction d'un bug de pretty-print.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1919 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 2b9271aca..4f17f081b 100644 --- a/tactics/Inv.v +++ b/tactics/Inv.v @@ -13,7 +13,7 @@ Require Export Equality. Declare ML Module "Inv" "Leminv". Syntax tactic level 0: - inversion [<<(Inv $ic $id)>>] -> [ (INVCOM $ic) [1 1] $id] +| inversion [<<(Inv $ic $id)>>] -> [ (INVCOM $ic) [1 1] $id] | inversion_in [<<(InvIn $ic $id ($LIST $l))>>] -> [ (INVCOM $ic) [1 1] $id (CLAUSE ($LIST $l))] @@ -28,9 +28,9 @@ Syntax tactic level 0: | inv_using_in [<<(UseInversionLemmaIn $id $c ($LIST $l))>>] -> ["Inversion " $id [1 1] "using " $c (CLAUSE ($LIST $l))] -| simple_inv [<<(INVCOM HalfInversion)>>] -> [ "Simple Inversion" ] -| inversion_com [<<(INVCOM Inversion)>>] -> [ "Inversion" ] -| inversion_clear [<<(INVCOM InversionClear)>>] -> [ "Inversion_clear" ]. +| simple_inv [<<(INVCOM "HalfInversion")>>] -> [ "Simple Inversion" ] +| inversion_com [<<(INVCOM "Inversion")>>] -> [ "Inversion" ] +| inversion_clear [<<(INVCOM "InversionClear")>>] -> [ "Inversion_clear" ]. Grammar tactic simple_tactic: ast := |