From 23545b802a14b2fad10f4382604c71f55b7d6d0e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 18 Oct 2015 19:44:49 +0200 Subject: Using appropriate lambda decomposition function counting let-ins when dealing with "match". Contrastingly, "fix" is considered not to count let-ins for finding the recursive argument (which is ok because the last argument is necessarily a lambda). --- pretyping/cases.ml | 5 +++-- pretyping/constr_matching.ml | 4 ++-- pretyping/detyping.ml | 2 +- 3 files changed, 6 insertions(+), 5 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 47d92f5e0..a5a7ace22 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1077,7 +1077,7 @@ let rec ungeneralize n ng body = let p = prod_applist p [mkRel (n+List.length sign+ng)] in it_mkLambda_or_LetIn (it_mkProd_or_LetIn p sign2) sign in mkCase (ci,p,c,Array.map2 (fun q c -> - let sign,b = decompose_lam_n_assum q c in + let sign,b = decompose_lam_n_decls q c in it_mkLambda_or_LetIn (ungeneralize (n+q) ng b) sign) ci.ci_cstr_ndecls brs) | App (f,args) -> @@ -1102,7 +1102,8 @@ let rec is_dependent_generalization ng body = | Case (ci,p,c,brs) -> (* We traverse a split *) Array.exists2 (fun q c -> - let _,b = decompose_lam_n_assum q c in is_dependent_generalization ng b) + let _,b = decompose_lam_n_decls q c in + is_dependent_generalization ng b) ci.ci_cstr_ndecls brs | App (g,args) -> (* We traverse an inner generalization *) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 121ab7488..5e99521a1 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -267,8 +267,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) -> - let ctx_b2,b2 = decompose_lam_n_assum ci.ci_cstr_ndecls.(0) b2 in - let ctx_b2',b2' = decompose_lam_n_assum ci.ci_cstr_ndecls.(1) b2' in + let ctx_b2,b2 = decompose_lam_n_decls ci.ci_cstr_ndecls.(0) b2 in + let ctx_b2',b2' = decompose_lam_n_decls ci.ci_cstr_ndecls.(1) b2' in let n = rel_context_length ctx_b2 in let n' = rel_context_length ctx_b2' in if noccur_between 1 n b2 && noccur_between 1 n' b2' then diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index a1213e72b..87f255024 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -302,7 +302,7 @@ and contract_branch isgoal e (cdn,can,mkpat,b) = let is_nondep_branch c l = try (* FIXME: do better using tags from l *) - let sign,ccl = decompose_lam_n_assum (List.length l) c in + let sign,ccl = decompose_lam_n_decls (List.length l) c in noccur_between 1 (rel_context_length sign) ccl with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *) false -- cgit v1.2.3