diff options
| author | herbelin | 2012-01-05 23:44:34 +0000 |
|---|---|---|
| committer | herbelin | 2012-01-05 23:44:34 +0000 |
| commit | 134f8741e0787d37bfdc082a5e3dddd2e1a3e62f (patch) | |
| tree | 49dbefc892e405043cb942ce0f84a730a027803e /interp/constrintern.ml | |
| parent | f629bd63917ca1fdacf5a3da4ee2ac7f3cba7398 (diff) | |
Backtracking on r14876 (fix for bug #2267): extra scopes might be
useful in the presence of coercions to Funclass. Fixed the bug
differently.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14880 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 656baa9465..3d39f0f928 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -731,9 +731,13 @@ let apply_scope_env env = function | [] -> {env with tmp_scope = None}, [] | sc::scl -> {env with tmp_scope = sc}, scl -let rec simple_adjust_scopes n = function - | [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) [] - | sc::scopes -> assert (n>0); sc :: simple_adjust_scopes (n-1) scopes +let rec simple_adjust_scopes n scopes = + (* Note: they can be less scopes than arguments but also more scopes *) + (* than arguments because extra scopes are used in the presence of *) + (* coercions to funclass *) + 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) = let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in |