diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index b62e31714f..6c7e1bbe5e 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -114,7 +114,8 @@ let type_inst_construct i (IndFamily (mis,globargs)) = let tc = mis_type_mconstruct i mis in prod_applist tc globargs -let type_of_existential env sigma c = Instantiate.existential_value sigma c +let type_of_existential env sigma c = + Instantiate.existential_type sigma (destEvar c) (* Case. *) |