diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 08:18:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 08:18:03 +0000 |
| commit | e9c8f69be0e0158d493b45476246cb82f7eb5d5a (patch) | |
| tree | 9f6f7fbbd844642daaa80b13407f97c8710c2c29 /translate/ppvernacnew.ml | |
| parent | f475ae32ed4ff6d4a48c6cbd94e2b6c28334ed42 (diff) | |
Passage de lconstr à constr pour les arguments immédiat de commandes
et tactiques; qqes bugs d'affichage; passage de la précédence des
projections de 10 à 9 avec associativité à gauche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4312 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate/ppvernacnew.ml')
| -rw-r--r-- | translate/ppvernacnew.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 491b8ab49..f5966a5cc 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -1008,10 +1008,12 @@ pr_vbinders bl ++ spc()) | Some r0 -> hov 2 (str"Eval" ++ spc() ++ pr_red_expr (pr_constr,pr_lconstr,pr_reference) r0 ++ - spc() ++ str"in" ++ spc () ++ pr_lconstr c) - | None -> hov 2 (str"Check" ++ spc() ++ pr_lconstr c) - in pr_mayeval r c - | VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_lconstrarg c) + spc() ++ str"in" ++ spc () ++ pr_constr c) + | None -> hov 2 (str"Check" ++ spc() ++ pr_constr c) + in + (if io = None then mt() else int (out_some io) ++ str ": ") ++ + pr_mayeval r c + | VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_constrarg c) | VernacPrint p -> let pr_printable = function | PrintFullContext -> str"Print All" |