From b2953849b999d1c3b42c0f494b234f2a93ac7754 Mon Sep 17 00:00:00 2001 From: pboutill Date: Thu, 14 Jun 2012 22:16:29 +0000 Subject: 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 --- interp/notation.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'interp/notation.mli') diff --git a/interp/notation.mli b/interp/notation.mli index 7629d86e7..3f66f993a 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -84,8 +84,8 @@ val declare_string_interpreter : scope_name -> required_module -> val interp_prim_token : loc -> prim_token -> local_scopes -> glob_constr * (notation_location * scope_name option) -val interp_prim_token_cases_pattern : loc -> prim_token -> name -> - local_scopes -> cases_pattern * (notation_location * scope_name option) +val interp_prim_token_cases_pattern_expr : loc -> (global_reference -> unit) -> prim_token -> + local_scopes -> raw_cases_pattern_expr * (notation_location * scope_name option) (** Return the primitive token associated to a [term]/[cases_pattern]; raise [No_match] if no such token *) -- cgit v1.2.3