diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-11 10:16:44 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-11 10:16:44 +0000 |
commit | eb067dc862c5a7acea2b92cabe867bfc9dcdaf92 (patch) | |
tree | fd2f4fb683561d027b803e03aa30820760c5f22f /lib/tlm.mli | |
parent | 9add74ea610a5b18d8ab7acc166dcefe73756981 (diff) |
Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).
Use two ways to solve it:
- added a whd_betaiota in solve_simple_eqn (since evarconv itself
refuses beta to preserve the opportunities of first-order-matching
expressions of the form "(fun x => P) t"; an advantage of this
whd_betaiota is also that it may simplify K-redexes.
- also added a last-chance test in case of failing occur-check by
trying to fully head-normalize (with delta) the right-hand-side
(allows to solve for instance "?n = id ?n" where id is a constant
(a bridled form of solve_refl that use fconv instead of evar_conv_x).
Incidentally improved a bit the rendering of the type of generalized
terms in pattern-matching by using whd_betaiota.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13113 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/tlm.mli')
0 files changed, 0 insertions, 0 deletions