diff options
Diffstat (limited to 'tactics/eauto.ml')
| -rw-r--r-- | tactics/eauto.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 6250fef2d..0869ac0c7 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -478,7 +478,7 @@ let unfold_head env (ids, csts) c = true, Environ.constant_value_in env c | App (f, args) -> (match aux f with - | true, f' -> true, Reductionops.whd_betaiota Evd.empty (mkApp (f', args)) + | true, f' -> true, Reductionops.whd_betaiota Evd.empty (EConstr.of_constr (mkApp (f', args))) | false, _ -> let done_, args' = Array.fold_left_i (fun i (done_, acc) arg -> |