diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-10 02:53:00 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-10 02:53:00 +0000 |
| commit | f88eba17b779c1a38e2ad332f9e4cc6bd04f57d6 (patch) | |
| tree | d71d22d5a8e92a34cb0e20f19ad4bb4fc9042ffe /syntax | |
| parent | df02bdb78e823db77605ed158a48b0fbd9312561 (diff) | |
Bug affichage LETPATTERN
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1567 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'syntax')
| -rw-r--r-- | syntax/PPTactic.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v index 5074dfd89..bdedb15c6 100644 --- a/syntax/PPTactic.v +++ b/syntax/PPTactic.v @@ -192,8 +192,10 @@ Syntax tactic | absurd [<<(Absurd $C)>>] -> ["Absurd " $C] | cut [<<(Cut $C)>>] -> ["Cut " $C] - | lettac [<<(LetTac $id $c (LETPATTERNS ($LIST $pl)))>>] -> - ["LetTac" [1 1] $id ":=" $c [1 1] "in" [1 1] (LETPATTERNS ($LIST $pl))] + | lettac_cons [<<(LetTac $id $c (LETPATTERNS $p ($LIST $pl)))>>] -> + ["LetTac" [1 1] $id ":=" $c [1 1] "in" [1 1] (LETPATTERNS $p ($LIST $pl))] + | lettac_nil [<<(LetTac $id $c (LETPATTERNS))>>] -> + ["LetTac" [1 1] $id ":=" $c] | left [<<(Left $b)>>] -> ["Left" (WITHBINDING $b)] | right [<<(Right $b)>>] -> [ "Right" (WITHBINDING $b)] |