diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-03-13 13:18:10 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-03-13 13:18:54 +0100 |
| commit | d868820ad1f00b896c5f44f18678fac2f8e0f720 (patch) | |
| tree | 2312a62d9fd275d1c70b5e4fabcbe308826d5a05 /intf | |
| parent | 7478ad7cc600753ba2609254657c87cacc27e8fc (diff) | |
Supporting "(@foo) args" in patterns, where "@foo" has no arguments.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 40812a3d8..f5855a971 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -40,15 +40,15 @@ type raw_cases_pattern_expr = | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t | RCPatCstr of Loc.t * Globnames.global_reference * raw_cases_pattern_expr list * raw_cases_pattern_expr list - (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *) + (** [CPatCstr (_, c, l1, l2)] represents (@c l1) l2 *) | RCPatAtom of Loc.t * Id.t option | RCPatOr of Loc.t * raw_cases_pattern_expr list type cases_pattern_expr = | CPatAlias of Loc.t * cases_pattern_expr * Id.t | CPatCstr of Loc.t * reference - * cases_pattern_expr list * cases_pattern_expr list - (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *) + * cases_pattern_expr list option * cases_pattern_expr list + (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *) | CPatAtom of Loc.t * reference option | CPatOr of Loc.t * cases_pattern_expr list | CPatNotation of Loc.t * notation * cases_pattern_notation_substitution |