diff options
Diffstat (limited to 'kernel/instantiate.ml')
| -rw-r--r-- | kernel/instantiate.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml index 627f0d45c1..9b1d9289a5 100644 --- a/kernel/instantiate.ml +++ b/kernel/instantiate.ml @@ -72,7 +72,7 @@ let existential_value sigma (n,args) = | Evar_empty -> anomaly "a defined existential with no body" -let const_abst_opt_value env sigma c = +let const_evar_opt_value env sigma c = match c with | DOPN(Const sp,_) -> if evaluable_constant env c then Some (constant_value env c) else None @@ -81,7 +81,5 @@ let const_abst_opt_value env sigma c = Some (existential_value sigma (ev,args)) else None - | DOPN(Abst sp,_) -> - if evaluable_abst env c then Some (abst_value env c) else None | _ -> invalid_arg "const_abst_opt_value" |