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

0 files changed, 0 insertions, 0 deletions