diff options
| author | msozeau | 2008-01-30 04:16:30 +0000 |
|---|---|---|
| committer | msozeau | 2008-01-30 04:16:30 +0000 |
| commit | 5eca868248b8faf8af73bd3bc015dea00a674752 (patch) | |
| tree | a279361f7870edc0662d8756220f1d9006301c16 | |
| parent | c10e6e3f2b2eec7350a1e9d9883191ed03f647d0 (diff) | |
Support for substructures in classes using :> notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10484 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_vernac.ml4 | 6 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 |
3 files changed, 7 insertions, 5 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index dacfd7329a..dd9dbb8e67 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -47,6 +47,7 @@ let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr" let thm_token = Gram.Entry.create "vernac:thm_token" let def_body = Gram.Entry.create "vernac:def_body" let typeclass_context = Gram.Entry.create "vernac:typeclass_context" +let of_type_with_opt_coercion = Gram.Entry.create "vernac:of_type_with_opt_coercion" let get_command_entry () = match Decl_mode.get_current_mode () with @@ -117,7 +118,8 @@ let no_coercion loc (c,x) = (* Gallina declarations *) GEXTEND Gram - GLOBAL: gallina gallina_ext thm_token def_body typeclass_context typeclass_constraint; + GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion + typeclass_context typeclass_constraint; gallina: (* Definition, Theorem, Variable, Axiom, ... *) @@ -525,7 +527,7 @@ GEXTEND Gram (* | id = identref -> id, CHole (loc, None) ] ] *) (* ; *) typeclass_field_type: - [ [ id = identref; ":"; t = lconstr -> id, t ] ] + [ [ id = identref; oc = of_type_with_opt_coercion; t = lconstr -> id, oc, t ] ] ; typeclass_field_def: [ [ id = identref; params = LIST0 identref; ":="; t = lconstr -> id, params, t ] ] diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 3502a9e86c..96b2a71673 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -694,8 +694,8 @@ let rec pr_vernac = function 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 ) - + prlist_with_sep (fun () -> str";" ++ spc()) + (fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props ) | VernacInstance (sup, (instid, bk, cl), props) -> hov 1 ( diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index cd9adf5cd9..3571b121b3 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -230,7 +230,7 @@ type vernac_expr = local_binder list * (* params *) sort_expr located * (* arity *) local_binder list * (* constraints *) - (lident * constr_expr) list (* props *) + (lident * bool * constr_expr) list (* props, with substructure hints *) | VernacInstance of local_binder list * (* super *) |