diff options
author | Stephane Glondu <steph@glondu.net> | 2012-03-27 07:48:23 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-03-27 07:48:23 +0200 |
commit | ad988252cac876f0b9998b5223f565d0a22aebb8 (patch) | |
tree | 0c0e0cd5c943b3fbeb97c99cf46e19bbc97144c0 /interp/constrintern.ml | |
parent | 11b04078a227fd8849972d05417487520177fb04 (diff) | |
parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) |
Merge tag 'upstream/8.3.pl4+dfsg'
Upstream version 8.3.pl4+dfsg
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r-- | interp/constrintern.ml | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4310a01e..96393659 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrintern.ml 14656 2011-11-16 08:46:31Z herbelin $ *) +(* $Id: constrintern.ml 15072 2012-03-20 17:36:33Z herbelin $ *) open Pp open Util @@ -693,8 +693,9 @@ let apply_scope_env (ids,unb,_,scopes) = function | [] -> (ids,unb,None,scopes), [] | sc::scl -> (ids,unb,sc,scopes), scl -let rec simple_adjust_scopes n = function - | [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) [] +let rec simple_adjust_scopes n scopes = + if n=0 then [] else match scopes with + | [] -> None :: simple_adjust_scopes (n-1) [] | sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) = @@ -771,9 +772,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 chop_aconstr_constructor loc (ind,k) args = if List.length args = 0 then (* Tolerance for a @id notation *) args else begin |