index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
enters coq_makefile2
Enrico Tassi
2017-05-23
*
test suite for coq_makefile2
Enrico Tassi
2017-05-23
*
coqdep: remove optimization making makefiles harder to write
Enrico Tassi
2017-05-23
*
ocamlfind: coqtop -config prints ocamlfind as found by ./configure
Enrico Tassi
2017-05-23
*
coqdep: set FOR_PACK variable for files that need to be packed
Enrico Tassi
2017-05-23
*
print_config: print COQ_SRC_SUBDIRS
Enrico Tassi
2017-05-23
*
Document --print-version in Usage
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
*
ide/project_fie.ml4: include standard banner with copyright
Enrico Tassi
2017-05-23
*
test suite for coq_makefile
Enrico Tassi
2017-05-23
*
configure: -local set coqdoc destination dir to ./doc rather than ""
Enrico Tassi
2017-05-23
*
Merge PR#661: Added a test for #4765 (an example of printing abbreviation wit...
Maxime Dénès
2017-05-23
|
\
*
\
Merge PR#659: Mention ./configure in INSTALL.doc
Maxime Dénès
2017-05-23
|
\
\
*
\
\
Merge PR#657: [test-suite] Add tests for goal printing.
Maxime Dénès
2017-05-23
|
\
\
\
*
\
\
\
Merge PR#646: Revised behavior on ill-formed identifiers
Maxime Dénès
2017-05-23
|
\
\
\
\
*
\
\
\
\
Merge PR#660: Change wrong bullet message.
Maxime Dénès
2017-05-23
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR#518: Faster universe unification
Maxime Dénès
2017-05-23
|
\
\
\
\
\
\
|
|
|
|
|
|
*
Added a test for #4765 (an example of printing abbreviation with binders).
Hugo Herbelin
2017-05-20
|
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
*
Deprecate -nodoc.
Théo Zimmermann
2017-05-20
|
|
*
|
|
|
Change wrong bullet message.
Théo Zimmermann
2017-05-20
|
|
|
*
|
|
Revised behavior on ill-formed identifiers.
Hugo Herbelin
2017-05-20
|
|
_
|
/
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR#276: Stopping injection not to work on discriminable atoms (see #4890).
Maxime Dénès
2017-05-20
|
\
\
\
\
\
|
|
|
|
|
*
Mention ./configure in INSTALL.doc
Théo Zimmermann
2017-05-20
|
|
|
|
|
/
|
|
|
|
/
|
*
|
|
|
|
Merge PR#654: Travis: do not cache opam logs (+prettier spacing)
Maxime Dénès
2017-05-20
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR#643: [ide] Disable `print_ast` call.
Maxime Dénès
2017-05-20
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR#474: A fix for #5390 (a useful error on used introduction names was ...
Maxime Dénès
2017-05-20
|
\
\
\
\
\
\
\
|
|
|
|
|
|
|
*
[test-suite] Add tests for goal printing.
Emilio Jesus Gallego Arias
2017-05-20
*
|
|
|
|
|
|
|
Merge PR#627: Obligations shrinking: shrink abstraction too
Maxime Dénès
2017-05-20
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR#644: [toplevel] [stm] Avoid edit_at in batch mode (bug #5520)
Maxime Dénès
2017-05-20
|
\
\
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
Merge PR#648: Allow interactive editing of `plugins/` by adding .dir-locals.el
Maxime Dénès
2017-05-20
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR#649: Fix a typo
Maxime Dénès
2017-05-20
|
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
Merge PR#651: Re-adding explicit dependency of misc universe test into all_st...
Maxime Dénès
2017-05-20
|
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
Merge PR#640: [toplevel] Restore 8.6 goal printing behavior.
Maxime Dénès
2017-05-20
|
\
\
\
\
\
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
Travis: do not cache opam logs (+prettier spacing)
Gaetan Gilbert
2017-05-19
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
Re-adding explicit dependency of misc universe test into all_stdlib.v.
Hugo Herbelin
2017-05-19
|
|
/
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
Fix a typo
Jason Gross
2017-05-18
|
|
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
Add .dir-locals.el to plugins
Jason Gross
2017-05-18
|
|
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
[toplevel] [stm] Avoid edit_at in batch mode (bug #5520)
Emilio Jesus Gallego Arias
2017-05-18
|
|
|
|
|
*
|
|
[ide] Disable `print_ast` call.
Emilio Jesus Gallego Arias
2017-05-18
|
|
|
|
_
|
/
/
/
|
|
|
/
|
|
|
|
|
|
|
|
*
|
|
A fix for #5390 (a useful error on used introduction names was masked).
Hugo Herbelin
2017-05-17
|
|
|
|
/
/
/
|
|
|
/
|
|
|
*
|
|
|
|
|
Merge PR#633: An extension of EXTEND and notations to make standard parsing t...
Maxime Dénès
2017-05-17
|
\
\
\
\
\
\
|
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
Documenting relaxing of constraints on injection.
Hugo Herbelin
2017-05-17
|
|
|
|
*
|
Stopping injection not to work on discriminable atoms (see #4890).
Hugo Herbelin
2017-05-17
|
|
_
|
_
|
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR#457: Adding an even more compact goal hyps mode.
Maxime Dénès
2017-05-17
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR#607: Make congruence reuse discriminate instead of rolling its own.
Maxime Dénès
2017-05-17
|
\
\
\
\
\
\
|
|
|
|
*
|
|
[toplevel] Restore 8.6 goal printing behavior.
Emilio Jesus Gallego Arias
2017-05-17
[next]
Enrico Tassi
Maxime Dénès
Hugo Herbelin
Théo Zimmermann
Emilio Jesus Gallego Arias
Gaetan Gilbert
Jason Gross
Jason Gross