diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/constrMatching.ml | 16 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 3 |
2 files changed, 8 insertions, 11 deletions
diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml index b0f1dd920a..270d274778 100644 --- a/pretyping/constrMatching.ml +++ b/pretyping/constrMatching.ml @@ -220,37 +220,37 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c = Array.fold_left2 (sorec stk env) subst args1 args22 else (* Might be a projection on the right *) match kind_of_term c2 with - | Proj (pr, c) -> + | Proj (pr, c) when not (Projection.unfolded pr) -> let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in sorec stk env subst p term | _ -> raise PatternMatchingFailure) | PApp (c1,arg1), App (c2,arg2) -> (match c1, kind_of_term c2 with - | PRef (ConstRef r), Proj (pr,c) when not (eq_constant r (Projection.constant pr)) -> + | PRef (ConstRef r), Proj (pr,c) when not (eq_constant r (Projection.constant pr)) + || Projection.unfolded pr -> raise PatternMatchingFailure | PProj (pr1,c1), Proj (pr,c) -> - if eq_constant (Projection.constant pr1) (Projection.constant pr) then + if Projection.equal 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) -> + | _, Proj (pr,c) when not (Projection.unfolded pr) -> let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in sorec stk env subst p term | _, _ -> try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c2) arg1 arg2 with Invalid_argument _ -> raise PatternMatchingFailure) - | PApp (PRef (ConstRef c1), _), Proj (pr, c2) when not (eq_constant c1 - (Projection.constant pr)) -> + | PApp (PRef (ConstRef c1), _), Proj (pr, c2) + when Projection.unfolded pr || not (eq_constant c1 (Projection.constant pr)) -> raise PatternMatchingFailure | PApp (c, args), Proj (pr, c2) -> let term = Retyping.expand_projection env sigma pr c2 [] in sorec stk env subst p term - | PProj (p1,c1), Proj (p2,c2) when - eq_constant (Projection.constant p1) (Projection.constant p2) -> + | PProj (p1,c1), Proj (p2,c2) when Projection.equal p1 p2 -> sorec stk env subst c1 c2 | PProd (na1,c1,d1), Prod(na2,c2,d2) -> diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index ab04a90459..bddd274efa 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -799,9 +799,6 @@ and whd_construct_stack env sigma s = sequence of products; fails if no delta redex is around *) -let match_eval_proj env proj = - ((lookup_constant proj env).Declarations.const_proj) - let try_red_product env sigma c = let simpfun = clos_norm_flags betaiotazeta env sigma in let rec redrec env x = |