diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-13 14:56:06 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-13 14:56:06 +0000 |
| commit | 6366dec0a76dbaf100907b2d4cd4da84a2ba7fef (patch) | |
| tree | 397f7ce5c437dd3a0b0d537c0d45b4fc7efb97ae /library/heads.ml | |
| parent | a07e31a2693bde01d3dca59364693096d550561a (diff) | |
Made unification patch 12268 even more ad hoc (if evars remain in a
term, its type is not the smallest one - actually, we would have to
reduce the term too but it would be more costly).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12274 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/heads.ml')
0 files changed, 0 insertions, 0 deletions