index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
names.ml
Commit message (
Expand
)
Author
Age
*
Allow using cumulativity without forcing strict constraints.
Gaëtan Gilbert
2018-03-09
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
[api] Miscellaneous consolidation + moves to engine.
Emilio Jesus Gallego Arias
2017-11-21
*
Use type nonrec in some functor arguments.
Gaëtan Gilbert
2017-10-16
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
A few typos.
Hugo Herbelin
2017-06-04
*
Creating a module Nameops.Name extending module Names.Name.
Hugo Herbelin
2017-05-31
*
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
*
Revised behavior on ill-formed identifiers.
Hugo Herbelin
2017-05-20
*
Remove some unused values and types
Gaetan Gilbert
2017-04-27
*
refactoring "Names.DirPath.is_empty" function
Matej Kosik
2017-04-20
*
refactoring "Names.DirPath.compare" function
Matej Kosik
2017-04-20
*
refactoring "Names.DirPath.equal" function
Matej Kosik
2017-04-20
*
Revert "refactoring: Names.DirPath.equal"
Matej Košík
2017-04-10
*
Revert "refactoring: Names.DirPath.compare"
Matej Košík
2017-04-10
*
Revert "refactoring: Names.DirPath.is_empty"
Matej Košík
2017-04-10
*
refactoring: Names.DirPath.is_empty
Matej Kosik
2017-04-10
*
refactoring: Names.DirPath.compare
Matej Kosik
2017-04-10
*
refactoring: Names.DirPath.equal
Matej Kosik
2017-04-10
*
[safe-string] Enable -safe-string !
Emilio Jesus Gallego Arias
2017-03-14
*
[safe_string] library/nameops
Emilio Jesus Gallego Arias
2017-03-14
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-12-07
|
\
|
*
Fix #5242 - Dubious unsilenceable warning on invalid identifier
Maxime Dénès
2016-12-02
*
|
COMMENT: Names.Cmap and Names.Cmap_env
Matej Kosik
2016-10-26
*
|
CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...
Matej Kosik
2016-08-30
*
|
Changing the definition of the "Lib.variable.info" type to enable us to do mo...
Matej Kosik
2016-08-24
|
/
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-30
|
\
|
*
A patch renaming equal into eq in the module dealing with
Hugo Herbelin
2016-03-22
|
*
Adding eq/compare/hash for syntactic view at
Hugo Herbelin
2016-03-22
*
|
ADD: Names.Name.is_{anonymous,name}
Matej Kosik
2016-02-18
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
COMMENTS: added to the "Names.inductive" and "Names.constructor" types.
Matej Kosik
2016-01-11
*
|
COMMENTS: added to the "Names" module.
Matej Kosik
2015-12-18
*
|
Better debug printers for module paths.
Maxime Dénès
2015-09-20
|
/
*
Reverting 16 last commits, committed mistakenly using the wrong push command.
Hugo Herbelin
2015-08-02
*
A patch renaming equal into eq in the module dealing with
Hugo Herbelin
2015-08-02
*
Adding eq/compare/hash for syntactic view at
Hugo Herbelin
2015-08-02
*
Followup of 9f81b58551.
Pierre-Marie Pédrot
2015-07-30
*
Fixing bug #4289 (hash-consing only user part of constant not
Hugo Herbelin
2015-07-30
*
Display functions for primitive projections.
Maxime Dénès
2015-07-02
*
Fixing bug #4190.
Pierre-Marie Pédrot
2015-04-16
*
Removing dead code.
Pierre-Marie Pédrot
2015-02-02
*
Correct restriction of vm_compute when handling universe polymorphic
Matthieu Sozeau
2015-01-15
*
Update headers.
Maxime Dénès
2015-01-12
*
Ensuring the good invariants of hashcons table generation in the API.
Pierre-Marie Pédrot
2014-12-17
*
Fix (actually, properly implement :) hashconsing of projections,
Matthieu Sozeau
2014-12-17
[next]