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.
---
 Makefile.build    | 2 +-
 tactics/eauto.ml4 | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index 57c22c6588..018471b684 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -59,7 +59,7 @@ CURDEPS:=$(addsuffix .d, $(CURFILES))
 VERBOSE=
 NO_RECOMPILE_ML4=
 NO_RECALC_DEPS=
-READABLE_ML4=true	# non-empty means .ml of .ml4 will be ascii instead of binary
+READABLE_ML4=	# non-empty means .ml of .ml4 will be ascii instead of binary
 VALIDATE=
 COQ_XML=	# is "-xml" when building XML library
 VM=		# is "-no-vm" to not use the vm"
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