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 /plugins/funind/glob_termops.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 'plugins/funind/glob_termops.mli')
| -rw-r--r-- | plugins/funind/glob_termops.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 179e8fe8d..84359a36b 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -19,7 +19,7 @@ val mkGVar : Id.t -> glob_constr val mkGApp : glob_constr*(glob_constr list) -> glob_constr val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr val mkGProd : Name.t * glob_constr * glob_constr -> glob_constr -val mkGLetIn : Name.t * glob_constr * glob_constr -> glob_constr +val mkGLetIn : Name.t * glob_constr * glob_constr option * glob_constr -> glob_constr val mkGCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr val mkGSort : glob_sort -> glob_constr val mkGHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *) |