From 9a48211ea8439a8502145e508b70ede9b5929b2f Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Thu, 27 Apr 2017 21:58:52 +0200
Subject: Post-rebase warnings (unused opens and 2 unused values)

---
 pretyping/constr_matching.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index d553506228..2334be9664 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
-- 
cgit v1.2.3