diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-07 20:17:32 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-07 20:17:32 +0000 |
| commit | a5808860fbabd1239d1116c2f4413d56ff99620f (patch) | |
| tree | bb71da65438e99980a727b8039dcaf3d3d96a06e /pretyping/pretyping.ml | |
| parent | 6cbd65aa4e5fe82259b44b89e5e624ed2299249c (diff) | |
Revert commit r13883: instantiating ?n by a lambda when "?n a" has to
be unified with a (truly) rigid term would need to be able to project
non-atomic arguments of evars what is not done (consider e.g.
"Check (fun m n (H:m+n=n) => ((f_equal _ H) : S (m+n) = S n)).").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13894 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretyping.ml')
0 files changed, 0 insertions, 0 deletions