diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-14 22:16:29 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-14 22:16:29 +0000 |
| commit | b2953849b999d1c3b42c0f494b234f2a93ac7754 (patch) | |
| tree | 5b836a93bca233337113f1695a519a9d7afa08b1 /interp/constrexpr_ops.mli | |
| parent | bc892142df9facc8347a513ba15e74c8b7a36289 (diff) | |
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
Diffstat (limited to 'interp/constrexpr_ops.mli')
| -rw-r--r-- | interp/constrexpr_ops.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 161320626..d3e32da46 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -19,6 +19,7 @@ open Constrexpr val constr_loc : constr_expr -> loc val cases_pattern_expr_loc : cases_pattern_expr -> loc +val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> loc val local_binders_loc : local_binder list -> loc @@ -50,3 +51,6 @@ val names_of_local_assums : local_binder list -> name located list (** Does not take let binders into account *) val names_of_local_binders : local_binder list -> name located list + +val raw_cases_pattern_expr_of_glob_constr : (Globnames.global_reference -> unit) + -> Glob_term.glob_constr -> raw_cases_pattern_expr |