aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/constr_matching.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/constr_matching.ml')
-rw-r--r--pretyping/constr_matching.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index d55350622..2334be966 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -87,7 +87,6 @@ let rec build_lambda sigma vars ctx m = match vars with
| n :: vars ->
(* change [ x1 ... xn y z1 ... zm |- t ] into
[ x1 ... xn z1 ... zm |- lam y. t ] *)
- let len = List.length ctx in
let pre, suf = List.chop (pred n) ctx in
let (na, t, suf) = match suf with
| [] -> assert false