diff options
| author | msozeau | 2008-01-07 22:46:48 +0000 |
|---|---|---|
| committer | msozeau | 2008-01-07 22:46:48 +0000 |
| commit | f76b61be82a4bb83fce667a613f5a4846582dc89 (patch) | |
| tree | f1281e4b706369da8d5860773e33eb89f972df94 /parsing/ppvernac.ml | |
| parent | 591e7ae9f979190a1ccaf9df523f6b73b1e6536a (diff) | |
Cleaner quantifiers for type classes, breaks clrewrite for the moment but implementation is much less add-hoc. Opens possibility of arbitrary prefixes in Class and Instance declarations. Current implementation with eauto is a bit more dangerous... next patch will fix it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10432 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/ppvernac.ml')
| -rw-r--r-- | parsing/ppvernac.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 1470f69027..0b889bf08d 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -696,7 +696,8 @@ let rec pr_vernac = function | VernacClass (id, par, ar, sup, props) -> hov 1 ( str"Class" ++ spc () ++ pr_lident id ++ - prlist_with_sep (spc) (pr_lident_constr (spc() ++ str ":" ++ spc())) par ++ +(* prlist_with_sep (spc) (pr_lident_constr (spc() ++ str ":" ++ spc())) par ++ *) + pr_and_type_binders_arg par ++ spc () ++ str":" ++ spc() ++ pr_rawsort (snd ar) ++ spc () ++ str"where" ++ spc () ++ prlist_with_sep (fun () -> str";" ++ spc()) (pr_lident_constr (spc () ++ str":" ++ spc())) props ) |