diff options
| author |  Samuel Mimram <samuel.mimram@ens-lyon.org> | 2005-01-31 14:34:14 +0000 |
|---|---|---|
| committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2005-01-31 14:34:14 +0000 |
| commit | 6497f27021fec4e01f2182014f2bb1989b4707f9 (patch) | |
| tree | 473be7e63895a42966970ab6a70998113bc1bd59 /translate/ppvernacnew.ml | |
| parent | 6b649aba925b6f7462da07599fe67ebb12a3460e (diff) | |
Imported Upstream version 8.0pl2upstream/8.0pl2
Diffstat (limited to 'translate/ppvernacnew.ml')
| -rw-r--r-- | translate/ppvernacnew.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 246253eb..bfcbee43 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppvernacnew.ml,v 1.95.2.2 2004/07/16 20:48:17 herbelin Exp $ *) +(* $Id: ppvernacnew.ml,v 1.95.2.3 2004/10/12 10:10:29 herbelin Exp $ *) open Pp open Names @@ -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 |