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 /proofs | |
| 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 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index effc8d4697..80bef43d81 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -177,9 +177,9 @@ let unify_0 mc wc m n = let whd_castappevar_stack sigma = let rec whrec x l = match x with - | DOPN(Evar ev,_) as c -> + | DOPN(Evar ev,args) as c -> if is_defined sigma ev then - whrec (existential_value sigma c) l + whrec (existential_value sigma (ev,args)) l else x,l | DOP2(Cast,c,_) -> whrec c l |