index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
/
globnames.ml
Commit message (
Expand
)
Author
Age
*
[api] Remove deprecated objects in engine / interp / library
Emilio Jesus Gallego Arias
2018-05-30
*
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-05-04
*
Allow using cumulativity without forcing strict constraints.
Gaëtan Gilbert
2018-03-09
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
Use r.(p) syntax to print primitive projections.
Maxime Dénès
2018-01-30
*
[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-11-06
*
[api] Deprecate all legacy uses of Name.Id in core.
Emilio Jesus Gallego Arias
2017-11-04
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into aspi...
Matthieu Sozeau
2016-04-04
|
\
*
\
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
\
|
*
|
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
|
COMMENTS: added to some variants of "Globalnames.global_reference" type.
Matej Kosik
2015-12-18
|
/
/
|
*
More uniformity in the style of comparison functions.
Arnaud Spiwack
2015-10-30
|
*
Make the code of compare functions linear in the number of constructors.
Arnaud Spiwack
2015-10-29
|
/
*
Removing dead code.
Pierre-Marie Pédrot
2015-02-02
*
Update headers.
Maxime Dénès
2015-01-12
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Missing equalities in Names-like structures.
Pierre-Marie Pédrot
2014-03-20
*
Using HMaps in global references.
Pierre-Marie Pédrot
2014-03-08
*
Fixing pervasive comparisons
Pierre-Marie Pédrot
2014-03-01
*
Partial application in Globnames.
ppedrot
2013-11-06
*
Removing some generic equalities.
ppedrot
2013-10-22
*
Added a more efficient way to recover the domain of a map.
ppedrot
2013-08-25
*
Names: shortcuts for building {kn, constant, mind} with empty sections
letouzey
2013-02-26
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Classops : avoid some use of Gmap
letouzey
2013-02-19
*
Names: revised representation of constants and mutual_inductive
letouzey
2013-02-19
*
Minor code cleanups, especially take advantage of Dir_path.is_empty
letouzey
2013-02-18
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Modulification of mod_bound_id
ppedrot
2012-12-18
*
Modulification of Label
ppedrot
2012-12-18
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
Finish patch for Hint Resolve, stopping to generate new constant names for
msozeau
2012-12-08
*
Monomorphization (library)
ppedrot
2012-11-22
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
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-09-14
*
Updating headers.
herbelin
2012-08-08
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29