diff options
| author | herbelin | 2012-01-04 14:56:33 +0000 |
|---|---|---|
| committer | herbelin | 2012-01-04 14:56:33 +0000 |
| commit | f629bd63917ca1fdacf5a3da4ee2ac7f3cba7398 (patch) | |
| tree | 8f596a8ac6005fdacae138d4c8fd9df8300e332e /interp/constrintern.ml | |
| parent | a760e7b562d742c77a3568c54a12997109b12c72 (diff) | |
Fixing Arguments Scope bug when too many scopes are given (bug #2667).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14876 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b161d001d2..656baa9465 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -733,7 +733,7 @@ let apply_scope_env env = function let rec simple_adjust_scopes n = function | [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) [] - | sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes + | sc::scopes -> assert (n>0); 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 |