index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
interp
/
impargs.ml
Age
Commit message (
Expand
)
Author
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-11-01
Add primitive float computation in Coq kernel
Guillaume Bertholon
2019-08-19
[api] Move handling of variable implicit data to impargs
Emilio Jesus Gallego Arias
2019-07-31
Specialize the section API.
Pierre-Marie Pédrot
2019-07-08
[api] Deprecate GlobRef constructors.
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-18
Merge PR #10134: Simplify impargs
Hugo Herbelin
2019-05-10
Remove ref from some implicit_discharge_request
Jasper Hugunin
2019-05-10
Simplify dispose_implicits
Jasper Hugunin
2019-05-10
[api] Remove 8.10 deprecations.
Emilio Jesus Gallego Arias
2019-03-14
Add relevance marks on binders.
Gaëtan Gilbert
2019-03-12
Merge PR #9389: Implement a method for manual declaration of implicits.
Emilio Jesus Gallego Arias
2019-02-28
Constructor type information uses the expanded form.
Pierre-Marie Pédrot
2019-02-28
Implement a method for manual declaration of implicits.
Jasper Hugunin
2019-02-18
Merge PR #9589: Deprecate duplicated explicitation_eq
Emilio Jesus Gallego Arias
2019-02-16
Deprecated duplicated explicitation_eq
Jasper Hugunin
2019-02-11
Fix #9508: Unexpected interaction between implicit arguments and primitive pr...
Pierre-Marie Pédrot
2019-02-04
Primitive integers
Maxime Dénès
2018-12-09
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Emilio Jesus Gallego Arias
2018-11-16
Termops.iter_constr_with_full_binders = EConstr.iter_with_full_binders
Gaëtan Gilbert
2018-10-19
Deprecating Global.type_of_global_in_context.
Hugo Herbelin
2018-10-05
[kernel] Remove section paths from `KerName.t`
Maxime Dénès
2018-09-12
Move maps & sets indexed by GlobRef.t into the kernel
Vincent Laporte
2018-07-24
Projections use index representation
Gaëtan Gilbert
2018-05-25
Remove some occurrences of Evd.empty
Maxime Dénès
2018-05-23
Collecting List.smart_* functions into a module List.Smart.
Hugo Herbelin
2018-05-04
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-04-05
Refactor impargs code.
Jasper Hugunin
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-12-30
Using a dedicated type for Lib.abstr_info.
Pierre-Marie Pédrot
2017-11-22
[api] Deprecate Term destructors, move to Constr
Emilio Jesus Gallego Arias
2017-11-13
[api] Another large deprecation, `Nameops`
Emilio Jesus Gallego Arias
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-09-28
Efficient fresh name generation relying on sets.
Pierre-Marie Pédrot
2017-07-26
Removing template polymorphism for definitions.
Pierre-Marie Pédrot
2017-07-19
[general] Move files to directories matching linking order.
Emilio Jesus Gallego Arias
