diff options
Diffstat (limited to 'kernel/instantiate.ml')
| -rw-r--r-- | kernel/instantiate.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml index 37ffa5ca12..f3634eac5b 100644 --- a/kernel/instantiate.ml +++ b/kernel/instantiate.ml @@ -82,7 +82,7 @@ let existential_type sigma c = let (n,args) = destEvar c in let info = Evd.map sigma n in let hyps = evar_hyps info in - instantiate_constr (ids_of_sign hyps) (body_of_type info.evar_concl) + instantiate_constr (ids_of_sign hyps) info.evar_concl (Array.to_list args) let existential_value sigma c = |