diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-12 10:13:28 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-12 10:13:28 +0000 |
| commit | 1f951ff0d587130039d425d8892a41d8126befd0 (patch) | |
| tree | 332d072abaa28bcee9be9dc4188f6904658c748f /translate | |
| parent | 30410fbb67dca41b66f98e5453627fb8071d2cbc (diff) | |
Mise en conformité de la syntaxe de Theorem/Lemma avec la doc: les lieurs sont autorisés avant l'énoncé
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6207 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppvernacnew.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index f4dce4cf0..085dcccb1 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -622,7 +622,7 @@ let rec pr_vernac = function hov 1 (pr_thm_token ki ++ spc() ++ pr_lident id ++ spc() ++ (match bl with | [] -> mt() - | _ -> error "Statements with local binders no longer supported") + | _ -> pr_binders bl ++ spc()) ++ str":" ++ pr_spc_type (rename_bound_variables (snd id) c)) | VernacEndProof Admitted -> str"Admitted" | VernacEndProof (Proved (opac,o)) -> (match o with |