index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
lib
Commit message (
Expand
)
Author
Age
*
use Int.equal instead of polymorphic =
Paul Steckler
2017-07-05
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-07-04
|
\
*
|
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
|
*
Fix bug 5392: Warnings defined in plugins are considered unknown
Maxime Dénès
2017-06-23
*
|
Merge PR#613: Cumulativity for inductive types
Maxime Dénès
2017-06-19
|
\
\
*
|
|
Fix typo in comment.
Maxime Dénès
2017-06-19
|
*
|
Fix bugs and add an option for cumulativity
Amin Timany
2017-06-16
|
/
/
*
|
Merge PR#375: Deprecation
Maxime Dénès
2017-06-15
|
\
\
*
\
\
Merge PR#739: completing a sentence in a comment
Maxime Dénès
2017-06-14
|
\
\
\
|
|
*
|
Remove support for Coq 8.4.
Guillaume Melquiond
2017-06-14
|
|
*
|
Remove support for Coq 8.3.
Guillaume Melquiond
2017-06-14
|
|
*
|
Remove support for Coq 8.2.
Guillaume Melquiond
2017-06-14
|
|
*
|
Add a version to be used when parsing compatibility notations mentioning old ...
Guillaume Melquiond
2017-06-14
|
|
/
/
|
/
|
|
*
|
|
Add support for "-bypass-API" argument of "coq_makefile"
Matej Košík
2017-06-12
|
*
|
completing a sentence in a comment
Matej Košík
2017-06-07
*
|
|
Put all plugins behind an "API".
Matej Kosik
2017-06-07
|
/
/
*
|
Merge PR#728: A few typos.
Maxime Dénès
2017-06-06
|
\
\
|
*
|
A few typos.
Hugo Herbelin
2017-06-04
*
|
|
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
|
/
/
*
|
[emacs] [toplevel] Make emacs flag local to the toplevel.
Emilio Jesus Gallego Arias
2017-06-01
|
*
Bump year in headers.
Maxime Dénès
2017-06-01
*
|
Merge PR#356: Making management of installation directories more structured, ...
Maxime Dénès
2017-05-30
|
\
\
*
\
\
Merge PR#692: Fail on deprecated warning even for Ocaml > 4.02.3
Maxime Dénès
2017-05-30
|
\
\
\
|
|
*
|
Relying on computation done in Envars to discover the installation directories.
Hugo Herbelin
2017-05-29
|
|
*
|
Generalizing to docdir and datadir the test for a relocated installation.
Hugo Herbelin
2017-05-29
|
|
*
|
Exporting the suffixes needed to build coqlib, docdir, etc.
Hugo Herbelin
2017-05-29
|
|
*
|
Using Coq_config.local rather than None to tell that Coq_config.coqlib is local.
Hugo Herbelin
2017-05-29
|
|
*
|
Configuration: always giving a value to configdir and datadir.
Hugo Herbelin
2017-05-29
|
|
*
|
Dead code (xdg_config_dirs).
Hugo Herbelin
2017-05-29
|
*
|
|
Fail on deprecated warning even for Ocaml > 4.02.3
Gaëtan Gilbert
2017-05-28
|
|
/
/
*
/
/
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
|
/
/
*
|
Merge PR#666: romega revisited : no more normalization trace, cleaned-up reso...
Maxime Dénès
2017-05-26
|
\
\
*
\
\
Merge PR#655: Extra functions exported in EConstr
Maxime Dénès
2017-05-26
|
\
\
\
*
\
\
\
Merge PR#645: [stm] Tweak debug options.
Maxime Dénès
2017-05-25
|
\
\
\
\
*
\
\
\
\
Merge PR#406: coq makefile2
Maxime Dénès
2017-05-25
|
\
\
\
\
\
*
|
|
|
|
|
[location] Renaming "CAst.ast" to "CAst.t"
Matej Košík
2017-05-24
*
|
|
|
|
|
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
\
\
\
\
\
|
|
*
|
|
|
|
coq_makefile: avoid spurious ./ in generated .conf file
Enrico Tassi
2017-05-23
|
|
*
|
|
|
|
enters coq_makefile2
Enrico Tassi
2017-05-23
|
|
*
|
|
|
|
ocamlfind: coqtop -config prints ocamlfind as found by ./configure
Enrico Tassi
2017-05-23
|
|
*
|
|
|
|
print_config: print COQ_SRC_SUBDIRS
Enrico Tassi
2017-05-23
|
|
*
|
|
|
|
Put the list of Coq sources subdirectories in one place
Enrico Tassi
2017-05-23
|
|
*
|
|
|
|
Usage.print_config moved to Envars
Enrico Tassi
2017-05-23
|
|
*
|
|
|
|
CoqProject_file: document in API deprecated features
Enrico Tassi
2017-05-23
|
|
*
|
|
|
|
CoqProject_file: API and code cleanup (tuples -> records)
Enrico Tassi
2017-05-23
|
|
*
|
|
|
|
ide/project_file.ml4 -> lib/coqProject_file.ml4 + .mli
Enrico Tassi
2017-05-23
|
|
/
/
/
/
/
|
|
|
|
*
/
Bigint.euclid: clarify which sign convention is used
Pierre Letouzey
2017-05-23
|
|
|
_
|
/
/
|
|
/
|
|
|
|
|
|
*
|
Moving "sym" on "eq" type to lib/util.ml.
Hugo Herbelin
2017-05-19
|
|
*
|
|
[stm] Tweak debug options.
Emilio Jesus Gallego Arias
2017-05-18
|
|
/
/
/
|
*
|
|
Documenting Option.List.find.
Hugo Herbelin
2017-05-05
[next]