diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-02-01 15:56:45 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-24 12:22:21 +0100 |
| commit | f9a4ca41bc1313300f5f9b9092fe24825f435706 (patch) | |
| tree | f2c6f100a01e26614a5ff6e7fe7471c7356b9de4 /pretyping/constr_matching.ml | |
| parent | 71cd2838bf3eb23a8f29df973d8012ebe2ec77b0 (diff) | |
Replacing "cast surgery" in LetIn by a proper field (see PR #404).
This is a patch fulfilling the relevant remark of Maxime that an
explicit information at the ML type level would be better than "cast
surgery" to carry the optional type of a let-in.
There are a very few semantic changes.
- a "(x:t:=c)" in a block of binders is now written in the more
standard way "(x:=c:t)"
- in notations, the type of a let-in is not displayed if not
explicitly asked so.
See discussion at PR #417 for more information.
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 |