Internalization of pattern is done in two phases.

First Notations, syntactic definitions, primitive entries are tackled to build
raw_cases_pattern_expr. Reference are revolved at this time too. Then raw_patterns
are internalized as cases_pattern or applied inductive (dealing with implicit
args, or_pattern refactoring, aliases).

It is more uniform, it allows notations for non fully applied constructors but :
 - It does not raise a warning when an identifier is also a global_reference
different than a constructor.
- It looks for implicit arguments twice. (because finding scopes of arguments
asks for implicit arguments).
- It does not deal anymore with constants that evaluates to constructor. (This one
  is voluntary, dealing with implicit & notations is already a hell full of bugs
  so what will be next step ? Any terms that computes to a pattern ???)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15439 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 4 deletions

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 6d3a5be39..a067440cb 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -96,10 +96,11 @@ let rec add_vars_of_simple_pattern globs = function
 	(UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here"))
   | CPatDelimiters (_,_,p) ->
       add_vars_of_simple_pattern globs p
-  | CPatCstr (_,_,pl) | CPatCstrExpl (_,_,pl) ->
-      List.fold_left add_vars_of_simple_pattern globs pl
-  | CPatNotation(_,_,(pl,pll)) ->
-      List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pll))
+  | CPatCstr (_,_,pl1,pl2) ->
+    List.fold_left add_vars_of_simple_pattern
+      (List.fold_left add_vars_of_simple_pattern globs pl1) pl2
+  | CPatNotation(_,_,(pl,pll),pl') ->
+      List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pl'::pll))
   | CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs
   |  _  -> globs