diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build index 57c22c658..018471b68 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 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 |