From 321a42bf24490b08e12af5d8c2cf627e01a25aba Mon Sep 17 00:00:00 2001
From: Cyprien Mangin <cyprien.mangin@m4x.org>
Date: Thu, 2 Feb 2017 18:45:28 +0100
Subject: Fix bindings handling of setoid_rewrite.

This fixes the discrepancy between "rewrite H with (1 := x)"
and "setoid_rewrite H with (1 := x)".
---
 proofs/clenv.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 0a90e0dbd..beed9e36b 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -661,7 +661,8 @@ let evar_of_binder holes = function
 | NamedHyp s -> evar_with_name holes s
 | AnonHyp n ->
   try
-    let h = List.nth holes (pred n) in
+    let nondeps = List.filter (fun hole -> not hole.hole_deps) holes in
+    let h = List.nth nondeps (pred n) in
     h.hole_evar
   with e when CErrors.noncritical e ->
     errorlabstrm "" (str "No such binder.")
-- 
cgit v1.2.3