diff options
| -rw-r--r-- | kernel/sign.ml | 6 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 4 | ||||
| -rw-r--r-- | pretyping/matching.ml | 3 | ||||
| -rw-r--r-- | tactics/inv.ml | 2 |
4 files changed, 9 insertions, 6 deletions
diff --git a/kernel/sign.ml b/kernel/sign.ml index 79619b48f..218ac6c48 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -181,7 +181,9 @@ let decompose_prod_n_assum n = prodec_rec empty_rel_context n (* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T - into the pair ([(xn,Tn);...;(x1,T1)],T) *) + into the pair ([(xn,Tn);...;(x1,T1)],T) + Lets in between are not expanded but turn into local definitions, + but n is the actual number of destructurated lambdas. *) let decompose_lam_n_assum n = if n < 0 then error "decompose_lam_n_assum: integer parameter must be positive"; @@ -189,7 +191,7 @@ let decompose_lam_n_assum n = if n=0 then l,c else match kind_of_term c with | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c - | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) (n-1) c + | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) n c | Cast (c,_,_) -> lamdec_rec l n c | c -> error "decompose_lam_n_assum: not enough abstractions" in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index c9e68d1e3..f0203fa2c 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -260,8 +260,8 @@ and contract_branch isgoal e (cn,mkpat,b) = let is_nondep_branch c n = try - let _,ccl = decompose_lam_n_assum n c in - noccur_between 1 n ccl + let sign,ccl = decompose_lam_n_assum n c in + noccur_between 1 (rel_context_length sign) ccl with _ -> (* Not eta-expanded or not reduced *) false diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 9ce8e703f..ada3b912b 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -161,7 +161,8 @@ let matches_core convert allow_partial_app pat c = | 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 n = List.length ctx and n' = List.length ctx' 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 let s = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx in let s' = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx' in diff --git a/tactics/inv.ml b/tactics/inv.ml index d8d7661be..baa77f9c4 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -117,7 +117,7 @@ let make_inv_predicate env sigma indf realargs id status concl = (* We lift to make room for the equations *) (hyps,lift nrealargs bodypred) in - let nhyps = List.length hyps in + let nhyps = rel_context_length hyps in let env' = push_rel_context hyps env in let realargs' = List.map (lift nhyps) realargs in let pairs = list_map_i (compute_eqn env' sigma nhyps) 0 realargs' in |