diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-03-12 15:30:51 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-03-12 15:30:51 +0000 |
| commit | 74db2b0098893a5912d7480a259ad91664a86120 (patch) | |
| tree | bf9c4fdff014b335c46684ffd211ce496a6f947c /pretyping | |
| parent | dba2ae9fa1eb01d795d36b209aee6045967ba00a (diff) | |
fixed confusion between number of cstr arguments and number of pattern variables (which include let-ins in cstr type)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12864 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 4 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 2 | ||||
| -rw-r--r-- | pretyping/matching.ml | 6 | ||||
| -rw-r--r-- | pretyping/pattern.ml | 2 |
4 files changed, 7 insertions, 7 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index d46fd226e..905bb49e0 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -237,7 +237,7 @@ let rec decomp_branch n nal b (avoid,env as e) c = let rec build_tree na isgoal e ci cl = let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name na rhs) in - let cnl = ci.ci_cstr_nargs in + let cnl = ci.ci_cstr_ndecls in List.flatten (list_tabulate (fun i -> contract_branch isgoal e (cnl.(i),mkpat i,cl.(i))) (Array.length cl)) @@ -409,7 +409,7 @@ let rec detype (isgoal:bool) avoid env t = (detype_eqns isgoal avoid env ci comp) is_nondep_branch avoid (ci.ci_ind,ci.ci_pp_info.style,ci.ci_npar, - ci.ci_cstr_nargs,ci.ci_pp_info.ind_nargs) + ci.ci_cstr_ndecls,ci.ci_pp_info.ind_nargs) (Some p) c bl | Fix (nvn,recdef) -> detype_fix isgoal avoid env nvn recdef | CoFix (n,recdef) -> detype_cofix isgoal avoid env n recdef diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 636f86224..3897b18e5 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -145,7 +145,7 @@ let make_case_info env ind style = let print_info = { ind_nargs = mip.mind_nrealargs_ctxt; style = style } in { ci_ind = ind; ci_npar = mib.mind_nparams; - ci_cstr_nargs = mip.mind_consnrealdecls; + ci_cstr_ndecls = mip.mind_consnrealdecls; ci_pp_info = print_info } let make_default_case_info env style ind = diff --git a/pretyping/matching.ml b/pretyping/matching.ml index d034bfae0..b94642c09 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -96,7 +96,7 @@ let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2 let same_case_structure (_,cs1,ind,_) ci2 br1 br2 = match ind with | Some ind -> ind = ci2.ci_ind - | None -> cs1 = ci2.ci_cstr_nargs + | None -> cs1 = ci2.ci_cstr_ndecls let matches_core convert allow_partial_app pat c = let conv = match convert with @@ -181,8 +181,8 @@ let matches_core convert allow_partial_app pat c = (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2 | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) -> - let ctx,b2 = decompose_lam_n_assum ci.ci_cstr_nargs.(0) b2 in - let ctx',b2' = decompose_lam_n_assum ci.ci_cstr_nargs.(1) b2' in + let ctx,b2 = decompose_lam_n_assum ci.ci_cstr_ndecls.(0) b2 in + let ctx',b2' = decompose_lam_n_assum ci.ci_cstr_ndecls.(1) b2' in let n = rel_context_length ctx in let n' = rel_context_length ctx' in if noccur_between 1 n b2 & noccur_between 1 n' b2' then diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 105672564..f9dec8f35 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -130,7 +130,7 @@ let pattern_of_constr sigma t = | Case (ci,p,a,br) -> let cip = ci.ci_pp_info in let no = Some (ci.ci_npar,cip.ind_nargs) in - PCase ((cip.style,ci.ci_cstr_nargs,Some ci.ci_ind,no), + PCase ((cip.style,ci.ci_cstr_ndecls,Some ci.ci_ind,no), pattern_of_constr p,pattern_of_constr a, Array.map pattern_of_constr br) | Fix f -> PFix f |