diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-09 11:27:47 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-09 11:27:47 +0000 |
| commit | 784363f5e6849fcba527e086ce6ebb21da13e87d (patch) | |
| tree | b1926c706ce4d8975c47e0d6c49610d96dfacf69 /interp | |
| parent | d82e4cc31064b543ba68f0f52a1c60128da0e539 (diff) | |
Correction bug List.map2 dans Case12.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10770 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 55f3d9fba..f45ceb87d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -436,12 +436,11 @@ 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 -let find_remaining_constructor_scopes pl1 (ind,j as cstr) = +let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) = let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in let npar = mib.Declarations.mind_nparams in - let nargs = Declarations.recarg_length mip.Declarations.mind_recargs j in snd (list_chop (List.length pl1 + npar) - (simple_adjust_scopes (npar+nargs) + (simple_adjust_scopes (npar + List.length pl2) (find_arguments_scope (ConstructRef cstr)))) (**********************************************************************) @@ -651,7 +650,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat = | CPatCstr (loc, head, pl) -> let c,idslpl1,pl2 = mustbe_constructor loc head intern_pat aliases pl scopes in check_constructor_length genv loc c idslpl1 pl2; - let argscs2 = find_remaining_constructor_scopes idslpl1 c in + let argscs2 = find_remaining_constructor_scopes idslpl1 pl2 c in let idslpl2 = List.map2 (intern_pat scopes ([],[])) argscs2 pl2 in let (ids',pll) = product_of_cases_patterns ids (idslpl1@idslpl2) in let pl' = List.map (fun (subst,pl) -> |