diff options
| author | herbelin | 2012-03-20 17:36:25 +0000 |
|---|---|---|
| committer | herbelin | 2012-03-20 17:36:25 +0000 |
| commit | 52b57c6c529d1896ee73890db9faf3d299619403 (patch) | |
| tree | aaeaf015290fb5b4174a844dc14922dde34fc98d /interp | |
| parent | 929885b46d19cb8e90507bf2f6bddc146a0458a9 (diff) | |
Fixing bug #2724 (using notations with binders in cases patterns
was provoking an anomaly instead of a regular error).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15070 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 3 | ||||
| -rw-r--r-- | interp/topconstr.ml | 8 | ||||
| -rw-r--r-- | interp/topconstr.mli | 4 |
3 files changed, 11 insertions, 4 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6b221ecd87..3890931274 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -868,9 +868,6 @@ let message_redundant_alias (id1,id2) = (* Expanding notations *) -let error_invalid_pattern_notation loc = - user_err_loc (loc,"",str "Invalid notation for pattern.") - let rec subst_pat_iterator y t (subst,p) = match p with | PatVar (_,id) as x -> if id = Name y then t else [subst,x] diff --git a/interp/topconstr.ml b/interp/topconstr.ml index db41809628..8db5b0afa2 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -924,7 +924,7 @@ let oldfashion_patterns = ref (true) let write_oldfashion_patterns = Goptions.declare_bool_option { Goptions.optsync = true; Goptions.optdepr = false; Goptions.optname = - "Constructors in atterns require all their arguments but no parameters instead of explicit parameters and arguments"; + "Constructors in patterns require all their arguments but no parameters instead of explicit parameters and arguments"; Goptions.optkey = ["Asymmetric";"Patterns"]; Goptions.optread = (fun () -> !oldfashion_patterns); Goptions.optwrite = (fun a -> oldfashion_patterns:=a); @@ -942,6 +942,12 @@ let names_of_local_binders bl = List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl) (**********************************************************************) +(* Miscellaneous *) + +let error_invalid_pattern_notation loc = + user_err_loc (loc,"",str "Invalid notation for pattern.") + +(**********************************************************************) (* Functions on constr_expr *) let constr_loc = function diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 337eb00472..b346655ad7 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -270,3 +270,7 @@ val ntn_loc : loc -> constr_notation_substitution -> string -> (int * int) list val patntn_loc : loc -> cases_pattern_notation_substitution -> string -> (int * int) list + +(** For cases pattern parsing errors *) + +val error_invalid_pattern_notation : Pp.loc -> 'a |