diff options
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b6fa25769..9c9350ab1 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -51,9 +51,9 @@ let unfold_projection env evd ts p c = let eval_flexible_term ts env evd c = match EConstr.kind evd c with - | Const (c,u as cu) -> + | Const (c, u) -> if is_transparent_constant ts c - then Option.map EConstr.of_constr (constant_opt_value_in env cu) + then Option.map EConstr.of_constr (constant_opt_value_in env (c, EInstance.kind evd u)) else None | Rel n -> (try match lookup_rel n env with |