diff options
| author | Hugo Herbelin | 2017-02-01 15:56:45 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-24 12:22:21 +0100 |
| commit | f9a4ca41bc1313300f5f9b9092fe24825f435706 (patch) | |
| tree | f2c6f100a01e26614a5ff6e7fe7471c7356b9de4 /intf/pattern.mli | |
| 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 'intf/pattern.mli')
| -rw-r--r-- | intf/pattern.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/pattern.mli b/intf/pattern.mli index 329ae837e1..a32e7e4b94 100644 --- a/intf/pattern.mli +++ b/intf/pattern.mli @@ -68,7 +68,7 @@ type constr_pattern = | PProj of projection * constr_pattern | PLambda of Name.t * constr_pattern * constr_pattern | PProd of Name.t * constr_pattern * constr_pattern - | PLetIn of Name.t * constr_pattern * constr_pattern + | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern | PSort of glob_sort | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern |