diff options
| author | Matthieu Sozeau | 2014-09-19 21:10:33 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-19 21:11:13 +0200 |
| commit | 9c2bbdd58b6935ea980e72289777a20b85fe4fdb (patch) | |
| tree | 0ba48b2b60ac76a3d3083001f327f077929202e8 /pretyping/constrMatching.ml | |
| parent | 2420cdec7290d070de3c7fcfb51caea2cc684d53 (diff) | |
Fixes in Ltac pattern-matching on primitive projections
and pretyping which was not contracting the eta-expanded forms in presence
of coercions.
Diffstat (limited to 'pretyping/constrMatching.ml')
| -rw-r--r-- | pretyping/constrMatching.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml index d4cbad054e..7af6396336 100644 --- a/pretyping/constrMatching.ml +++ b/pretyping/constrMatching.ml @@ -229,7 +229,11 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c = (match c1, kind_of_term c2 with | PRef (ConstRef r), Proj (pr,c) when not (eq_constant r pr) -> raise PatternMatchingFailure - (* eta-expanded version of projection against projection *) + | PProj (pr1,c1), Proj (pr,c) -> + if eq_constant pr1 pr then + try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c) arg1 arg2 + with Invalid_argument _ -> raise PatternMatchingFailure + else raise PatternMatchingFailure | _, Proj (pr,c) -> let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in sorec stk env subst p term |