aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/vernacexpr.ml9
1 files changed, 1 insertions, 8 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index eaa434956f..e563f66874 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -237,14 +237,7 @@ type vernac_expr =
| VernacIdentityCoercion of locality * lident *
class_rawexpr * class_rawexpr
- (* Type classes *)
-(* | VernacClass of *)
-(* lident * (\* name *\) *)
-(* local_binder list * (\* params *\) *)
-(* sort_expr located option * (\* arity *\) *)
-(* local_binder list * (\* constraints *\) *)
-(* (lident * bool * constr_expr) list (\* props, with substructure hints *\) *)
-
+ (* Type classes *)
| VernacInstance of
bool * (* global *)
local_binder list * (* super *)