diff options
| author | herbelin | 2000-05-25 15:00:43 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-25 15:00:43 +0000 |
| commit | 36c150fac098e1a038d23b812744e1aaaa5993da (patch) | |
| tree | b062f1c9500c584b65fd234580da1b78f05a6539 /kernel/typeops.ml | |
| parent | bfb42267924cbdafc101ac1cab55ace5e2733bfb (diff) | |
Bug existential_value au lieu de existential_type + divers sur existential
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@476 85f007b7-540e-0410-9357-904b9bb8a0f7
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. *) |