From 3366f05ab09aa90dcc96d7432bff09617162c3e4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 13 Mar 2016 17:49:25 +0100
Subject: Adopting the same rules for interpreting @, abbreviations and
 notations in patterns than in terms, wrt implicit arguments and scopes.

See file Notations2.v for the conventions in use in terms.

Somehow this could be put in 8.5 since it puts in agreement the
interpretation of abbreviations and notations in "symmetric patterns"
to what is done in terms (even though the interpretation rules for
terms are a bit ad hoc).

There is one exception: in terms, "(foo args) args'" deactivates the
implicit arguments and scopes in args'. This is a bit complicated to
implement in patterns so the syntax is not supported (and anyway, this
convention is a bit questionable).
---
 intf/constrexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index f5855a971e..efd5129b66 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -40,7 +40,7 @@ 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 (_, 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
 
-- 
cgit v1.2.3