From b3192497979a57a6078b2ecdb0d8b546cb100ffa Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Fri, 10 Apr 2015 19:22:12 +0200
Subject: Fix compilation broken by Matthieu's last commit.

 Btw, also unset the READABLE_ML4 option, which probably caused
 this issue. No, we normally do *not* want to see the internals
 of .ml generated out of a .ml4 (except during some specific debug
 sessions). It is *so* easy otherwise to edit the wrong .ml by
 mistake and forget to edit the original .ml4.
---
 tactics/eauto.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 1d89286af1..7af43e6062 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -568,7 +568,7 @@ let autounfold_one db cl =
   in
     if did then
       match cl with
-      | Some hyp -> change_in_hyp None (fun sigma -> sigma, c') hyp
+      | Some hyp -> change_in_hyp None (make_change_arg c') hyp
       | None -> convert_concl_no_check c' DEFAULTcast
     else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
   end
-- 
cgit v1.2.3