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 /interp/smartlocate.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 'interp/smartlocate.ml')
| -rw-r--r-- | interp/smartlocate.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 178c1c1f9..d863e0561 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -28,7 +28,7 @@ let global_of_extended_global_head = function | NRef ref -> ref | NApp (rc, _) -> head_of rc | NCast (rc, _) -> head_of rc - | NLetIn (_, _, rc) -> head_of rc + | NLetIn (_, _, _, rc) -> head_of rc | _ -> raise Not_found in head_of syn_def |