index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
interp
/
impargs.mli
Age
Commit message (
Expand
)
Author
2020-08-28
When reporting an implicit argument error on a rename argument, use the renam...
Hugo Herbelin
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-02-04
Add syntax for non maximally inserted implicit arguments
SimonBoulier
2019-12-04
Impargs: Using ExplByPos/ExplByName rather than encoding index as an ident.
Hugo Herbelin
2019-11-21
[coq] Untabify the whole ML codebase.
Emilio Jesus Gallego Arias
2019-08-19
[api] Move handling of variable implicit data to impargs
Emilio Jesus Gallego Arias
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-06-16
Turning "manual_implicits" into a list of position in impargs.ml.
Hugo Herbelin
2019-06-16
Adding location in warning telling implicit arguments differ in term and type.
Hugo Herbelin
2019-05-23
Fixing typos - Part 2
JPR
2019-05-10
[api] Remove 8.10 deprecations.
Emilio Jesus Gallego Arias
2019-02-28
Implement a method for manual declaration of implicits.
Jasper Hugunin
2019-02-16
Deprecated duplicated explicitation_eq
Jasper Hugunin
2018-12-09
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Emilio Jesus Gallego Arias
2018-05-04
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-03-28
[api] Deprecate a couple of aliases that we missed.
Emilio Jesus Gallego Arias
2018-03-05
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-02-28
[econstr] Continue consolidation of EConstr API under `interp`.
Emilio Jesus Gallego Arias
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-07-19
[general] Move files to directories matching linking order.
Emilio Jesus Gallego Arias
