diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-09 21:26:09 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-09 21:31:38 +0200 |
| commit | 9861690aefc7d63641c1827cce2701b692c146e3 (patch) | |
| tree | b907ff09c2bebc570c59a1362dda2c346dfb8c30 | |
| parent | b3d64ad3164517ee0eeb148c2f1d6c44eb9cf23d (diff) | |
Allow pattern matching on the applied form of projections with primitive
applications, solving part of bug #3503.
| -rw-r--r-- | pretyping/constrMatching.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml index 21e22e0bb..423ce4cb1 100644 --- a/pretyping/constrMatching.ml +++ b/pretyping/constrMatching.ml @@ -210,7 +210,14 @@ let matches_core convert allow_partial_app allow_bound_rels pat c = | _ -> (try Array.fold_left2 (sorec stk) (sorec stk subst c1 c2) arg1 arg2 with Invalid_argument _ -> raise PatternMatchingFailure)) - + + | PApp (PRef (ConstRef c1),arg1), Proj (p2,c2) when eq_constant c1 p2 -> + let pb = Environ.lookup_projection p2 (Global.env ()) in + let pars = pb.Declarations.proj_npars in + if Array.length arg1 == pars + 1 then + sorec stk subst arg1.(pars) c2 + else raise PatternMatchingFailure + | PProj (p1,c1), Proj (p2,c2) when eq_constant p1 p2 -> sorec stk subst c1 c2 |