diff options
| author | barras | 2004-01-16 10:25:17 +0000 |
|---|---|---|
| committer | barras | 2004-01-16 10:25:17 +0000 |
| commit | 6d7067289aacb00702a687c7a3242d40b7405315 (patch) | |
| tree | fdc803bab5b64773442f5b715cc95f7922bf830d | |
| parent | 8f800080589eae50d4eee7a2166423f5bc9e386c (diff) | |
Corrige: Intros [] etait traduit intros (), qui ne reparse pas
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5211 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | translate/pptacticnew.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 5e0cc68bac..b4002994fe 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -213,7 +213,7 @@ let rec pr_intro_pattern = function | IntroIdentifier id -> pr_id id and pr_case_intro_pattern = function - | [pl] -> + | [_::_ as pl] -> str "(" ++ hv 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")" | pll -> str "[" ++ |