diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-06 09:29:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-06 09:29:20 +0000 |
| commit | 64c9874e12872a08bfcce470b5e03813c5cff586 (patch) | |
| tree | 42a6e0060354c7f9327fd8349e0c1c8394ae7ccf /parsing/ppvernac.ml | |
| parent | 9953deaa45c642301a6cd7202b486c45923dece8 (diff) | |
Correction terminologie et ajout plage unicode 1D400-1D7FF (mathematical
alphanumerical symbols) suite à remarques de Arnaud.
Correction bugs d'affichage de l'option -translate.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11059 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/ppvernac.ml')
| -rw-r--r-- | parsing/ppvernac.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index c4b5c2d3e..3ec225ddc 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -534,11 +534,13 @@ let rec pr_vernac = function | Some cc -> str" :=" ++ spc() ++ cc)) | VernacStartTheoremProof (ki,l,_,_) -> - hov 1 (pr_thm_token ki ++ spc() ++ - prlist_with_sep (fun () -> str "with ") (fun (id,(bl,c)) -> hov 0 - (pr_opt pr_lident id ++ spc() ++ - (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ - str":" ++ pr_spc_lconstr c)) l) + let pr_statement head (id,(bl,c)) = + hov 0 + (head ++ spc () ++ pr_opt pr_lident id ++ spc() ++ + (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ + str":" ++ pr_spc_lconstr c) in + hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++ + prlist (pr_statement (str "with ")) (List.tl l)) | VernacEndProof Admitted -> str"Admitted" | VernacEndProof (Proved (opac,o)) -> (match o with @@ -821,7 +823,7 @@ let rec pr_vernac = function | VernacDeclareImplicits (local,q,None) -> hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q) | VernacDeclareImplicits (local,q,Some imps) -> - hov 1 (str"Implicit Arguments" ++ pr_non_globality local ++ + hov 1 (str"Implicit Arguments " ++ pr_non_globality local ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") | VernacReserve (idl,c) -> |