diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-18 19:44:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-18 20:11:13 +0200 |
| commit | 23545b802a14b2fad10f4382604c71f55b7d6d0e (patch) | |
| tree | 95bc8d0717964c3d8a276735393b80b3f055b935 /pretyping | |
| parent | 14edc57ac5ad75bbc4ea8559111606aea8978f48 (diff) | |
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).
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 5 | ||||
| -rw-r--r-- | pretyping/constr_matching.ml | 4 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 2 |
3 files changed, 6 insertions, 5 deletions
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 |