diff options
| author | msozeau | 2008-03-21 16:20:59 +0000 |
|---|---|---|
| committer | msozeau | 2008-03-21 16:20:59 +0000 |
| commit | 123c8683a25b34070d4874df4cdd9381d5ceac24 (patch) | |
| tree | 58b51cbd58bc8492d2b79985f917d49dccefd567 /interp/implicit_quantifiers.ml | |
| parent | 78e8a11a5f40c5ee1c09e279350ab208c4a31b64 (diff) | |
Correct bug introduced in r10589, where we lost information that
assumption types are types when type-checking them and necessary
coercions were not inserted. Add empty_evar_defs definition in Evd and
call the new helper function in constrintern that performs
interpretation and gives back implicit argument information.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10706 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions