diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-04-10 19:22:12 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-04-10 19:22:12 +0200 |
| commit | b3192497979a57a6078b2ecdb0d8b546cb100ffa (patch) | |
| tree | 2c1db3bd33bed59d2aba826d8dcb6b6372a3b70f /tactics | |
| parent | a86ae4d352cc8e4ac306f04d5536d7fff04d3303 (diff) | |
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.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eauto.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 1d89286af..7af43e606 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 |