diff options
Diffstat (limited to 'pretyping/constr_matching.ml')
| -rw-r--r-- | pretyping/constr_matching.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 5ec44a68d..1cae8d16d 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -264,7 +264,11 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels sorec ((na1,na2,c2)::ctx) (Environ.push_rel (LocalAssum (na2,c2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 - | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) -> + | PLetIn (na1,c1,Some t1,d1), LetIn(na2,c2,t2,d2) -> + sorec ((na1,na2,t2)::ctx) (Environ.push_rel (LocalDef (na2,c2,t2)) env) + (add_binders na1 na2 binding_vars (sorec ctx env (sorec ctx env subst c1 c2) t1 t2)) d1 d2 + + | PLetIn (na1,c1,None,d1), LetIn(na2,c2,t2,d2) -> sorec ((na1,na2,t2)::ctx) (Environ.push_rel (LocalDef (na2,c2,t2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 |