diff options
author | 2010-06-11 10:16:44 +0000 | |
---|---|---|
committer | 2010-06-11 10:16:44 +0000 | |
commit | eb067dc862c5a7acea2b92cabe867bfc9dcdaf92 (patch) | |
tree | fd2f4fb683561d027b803e03aa30820760c5f22f /pretyping/cases.ml | |
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 'pretyping/cases.ml')
-rw-r--r-- | pretyping/cases.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 64ad1801f..540db1c81 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1024,6 +1024,7 @@ let rec generalize_problem names pb = function | [] -> pb | i::l -> let d = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in + let d = on_pi3 (whd_betaiota !(pb.evdref)) d in (* for better rendering *) let pb' = generalize_problem names pb l in let tomatch = lift_tomatch_stack 1 pb'.tomatch in let tomatch = regeneralize_index_tomatch (i+1) tomatch in |