aboutsummaryrefslogtreecommitdiff
path: root/kernel/typeops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/typeops.ml')
-rw-r--r--kernel/typeops.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 5b6d45b748..ae1bb46cfa 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -94,8 +94,8 @@ let type_of_constructor env sigma cstr =
(index_of_constructor cstr)
(inductive_of_constructor cstr)
-let type_of_existential env sigma c =
- Instantiate.existential_type sigma (destEvar c)
+let type_of_existential env sigma ev =
+ Instantiate.existential_type sigma ev
(* Case. *)