diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 16 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 4 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 2 |
4 files changed, 13 insertions, 11 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 6b6b4871cf..3f437721a8 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -409,17 +409,19 @@ GEXTEND Gram ; typeclass_constraint_binder: [ [ tc = typeclass_constraint -> - let (n,bk,t) = tc in - LocalRawAssum ([n], TypeClass bk, t) + let (n,(b,b'),t) = tc in + LocalRawAssum ([n], TypeClass (b,b'), t) ] ] ; typeclass_constraint: - [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), Explicit, c - | iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" -> - (loc, Name iid), expl, c - | c = operconstr LEVEL "200" -> - (loc, Anonymous), Implicit, c + [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), (Implicit, Explicit), c + | "{"; id = name; "}"; ":" ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" -> + id, (Implicit, expl), c + | iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" -> + (loc, Name iid), (Explicit, expl), c + | c = operconstr LEVEL "200" -> + (loc, Anonymous), (Implicit, Implicit), c ] ] ; diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index aaf4324e2c..19cb287781 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -166,7 +166,7 @@ module Constr : val binder_let : local_binder list Gram.Entry.e val binders_let : local_binder list Gram.Entry.e val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e - val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e + val typeclass_constraint : (name located * (binding_kind * binding_kind) * constr_expr) Gram.Entry.e val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e end diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 04b700236a..912406f3f1 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -219,13 +219,13 @@ let surround_binder k p = match k with Default Explicit -> hov 1 (str"(" ++ p ++ str")") | Default Implicit -> hov 1 (str"{" ++ p ++ str"}") - | TypeClass b -> hov 1 (str"[" ++ p ++ str"]") + | TypeClass _ -> hov 1 (str"[" ++ p ++ str"]") let surround_implicit k p = match k with Default Explicit -> p | Default Implicit -> (str"{" ++ p ++ str"}") - | TypeClass b -> (str"[" ++ p ++ str"]") + | TypeClass _ -> (str"[" ++ p ++ str"]") let pr_binder many pr (nal,k,t) = match t with diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index e27a93b33e..6bd795ed5f 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -139,7 +139,7 @@ let mlexpr_of_binding_kind = function let mlexpr_of_binder_kind = function | Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >> - | Topconstr.TypeClass b -> <:expr< Topconstr.TypeClass $mlexpr_of_binding_kind b$ >> + | Topconstr.TypeClass (b,b') -> <:expr< Topconstr.TypeClass $mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_binding_kind (b,b')$ >> let rec mlexpr_of_constr = function | Topconstr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) -> |