From 66892881c69cfb91fe1cd772cd88ac2c73c99bbe Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 17 Oct 2018 17:10:32 +0200
Subject: Fix warning unused variable

---
 pretyping/evarconv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 96d7cff152..7b510cfd5c 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -768,7 +768,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
              Feedback.msg_notice (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in
   match (flex_kind_of_term flags env evd term1 sk1,
          flex_kind_of_term flags env evd term2 sk2) with
-    | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
+    | Flexible (sp1,al1), Flexible (sp2,al2) ->
         (* sk1[?ev1] =? sk2[?ev2] *)
         let f1 i = first_order env i term1 term2 sk1 sk2
 	and f2 i =
-- 
cgit v1.2.3