index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
/
arguments_renaming.ml
Age
Commit message (
Expand
)
Author
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-02-02
Move kind_of_type from the kernel to ssr.
Pierre-Marie Pédrot
2019-11-21
[coq] Untabify the whole ML codebase.
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-03-14
Add relevance marks on binders.
Gaëtan Gilbert
2019-01-20
Discard argument names of section variables on section close
Jasper Hugunin
2018-12-18
[arguments] cleanup
Enrico Tassi
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-05-04
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
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-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-16
Clean up universes of constants and inductives
Amin Timany
2016-10-29
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-27
Complete overhaul of the Arguments vernacular.
Maxime Dénès
2016-08-30
CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...
Matej Kosik
2016-08-24
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
CLEANUP: removing superfluous (module) qualifiers
Matej Kosik
2016-08-24
Changing the definition of the "Lib.variable.info" type to enable us to do mo...
Matej Kosik
2016-01-20
Update copyright headers.
Maxime Dénès
2015-01-12
Update headers.
Maxime Dénès
2014-08-03
Move to a representation of universe polymorphic constants using indices for ...
Matthieu Sozeau
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2013-04-22
code simplifications concerning Summary
letouzey
2013-04-18
Fix #3001 (rename arg of global cst inside section)
gareuselesinge
2012-12-18
Modulification of name
ppedrot
2012-09-14
Partial revert of Yann commit in order to use CLib.List when opening
ppedrot
2012-09-14
This patch removes unused "open" (automatically generated from
regisgia
2012-08-08
Updating headers.
herbelin
2012-05-29
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-03-02
Noise for nothing
pboutill
2011-11-21
Renamig support added to "Arguments"
gareuselesinge