diff options
Diffstat (limited to 'tactics/eauto.ml')
| -rw-r--r-- | tactics/eauto.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index e0dff3739..8d1e0e507 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -472,8 +472,9 @@ let unfold_head env sigma (ids, csts) c = (match Environ.named_body id env with | Some b -> true, EConstr.of_constr b | None -> false, c) - | Const (cst,u as c) when Cset.mem cst csts -> - true, EConstr.of_constr (Environ.constant_value_in env c) + | Const (cst, u) when Cset.mem cst csts -> + let u = EInstance.kind sigma u in + true, EConstr.of_constr (Environ.constant_value_in env (cst, u)) | App (f, args) -> (match aux f with | true, f' -> true, Reductionops.whd_betaiota sigma (mkApp (f', args)) |