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/instantiate.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/instantiate.ml')
| -rw-r--r-- | kernel/instantiate.ml | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml index 94ab793c6a..7a929b9fa3 100644 --- a/kernel/instantiate.ml +++ b/kernel/instantiate.ml @@ -58,15 +58,13 @@ let constant_value env cst = let name_of_existential n = id_of_string ("?" ^ string_of_int n) -let existential_type sigma c = - let (n,args) = destEvar c in +let existential_type sigma (n,args) = let info = Evd.map sigma n in let hyps = evar_hyps info in (* TODO: check args [this comment was in Typeops] *) instantiate_constr (ids_of_sign hyps) info.evar_concl (Array.to_list args) -let existential_value sigma c = - let (n,args) = destEvar c in +let existential_value sigma (n,args) = let info = Evd.map sigma n in let hyps = evar_hyps info in match info.evar_body with @@ -79,9 +77,9 @@ let const_abst_opt_value env sigma c = match c with | DOPN(Const sp,_) -> if evaluable_constant env c then Some (constant_value env c) else None - | DOPN(Evar ev,_) -> + | DOPN(Evar ev,args) -> if Evd.is_defined sigma ev then - Some (existential_value sigma c) + Some (existential_value sigma (ev,args)) else None | DOPN(Abst sp,_) -> |