From a86ae4d352cc8e4ac306f04d5536d7fff04d3303 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 10 Apr 2015 18:28:12 +0200
Subject: Fix #3590 for good this time, by changing the API, change's argument
 now takes a variable substitution for matched variables in the (lhs) pattern,
 and uses the existing ist structure to pretype the rhs correcly, without
 having to deal with the volatile evars.

---
 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 b1cbea51c8..86b5e414fe 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -675,7 +675,7 @@ let mkDestructEq :
      [Simple.generalize new_hyps;
       (fun g2 ->
 	Proofview.V82.of_tactic (change_in_concl None
-	  (fun sigma ->
+	  (fun patvars 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