From 4c576db3ed40328caa37144eb228365f497293e5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 15 Nov 2014 22:13:28 +0100
Subject: Fixing side bug in db37c9f3f32ae7 delaying interpretation of the
 right-hand side of a "change with": the rhs lives in the toplevel
 environment.

---
 plugins/funind/recdef.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 72613624ba..fd54584bc8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -674,7 +674,7 @@ let mkDestructEq :
      [Simple.generalize new_hyps;
       (fun g2 ->
 	change_in_concl None
-	  (fun env sigma -> 
+	  (fun sigma ->
 	    pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2)) g2);
       Proofview.V82.of_tactic (simplest_case expr)]), to_revert
 
-- 
cgit v1.2.3