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
*
Fixing a collision about the meta-variable ".." in recursive notations.
Hugo Herbelin
2016-07-16
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-07-13
|
\
|
*
Fixing printing of evar name in an error message of instantiate.
Hugo Herbelin
2016-07-13
|
*
Typo.
Hugo Herbelin
2016-07-13
*
|
Makefile.dev: fix a typo in the 'logic' rule
Pierre Letouzey
2016-07-13
*
|
Makefile.build: follow-up of commits by Matej on VERBOSE and READABLE_ML4
Pierre Letouzey
2016-07-12
*
|
.gitignore: no more generated grammar/*.ml files
Pierre Letouzey
2016-07-12
*
|
Makefile: no more .ml4.d hence no more rule to clean them
Pierre Letouzey
2016-07-12
*
|
".gitignore" update
Matej Kosik
2016-07-12
*
|
removing ocamldoc-related syntax errors
Matej Kosik
2016-07-12
*
|
expanding "make help" a little bit
Matej Kosik
2016-07-12
*
|
Removing "READABLE_ML4=" from "Makefile.build"
Matej Kosik
2016-07-12
*
|
Removing "VERBOSE=" from "Makefile.build"
Matej Kosik
2016-07-11
*
|
Fixing the printing of unknown locations by adding a newline.
Pierre-Marie Pédrot
2016-07-08
*
|
Adding a breaking space in warning names.
Pierre-Marie Pédrot
2016-07-08
*
|
Remove spurious warnings about projections when requiring modules.
Pierre-Marie Pédrot
2016-07-08
|
*
Add a few fixes in CHANGES that were forgotten.
Maxime Dénès
2016-07-08
|
*
Fix test file for #4858.
Maxime Dénès
2016-07-08
*
|
Fixing #4906 (regression in printing an error message).
Hugo Herbelin
2016-07-08
*
|
Typo in a comment of stdlib.
Hugo Herbelin
2016-07-08
|
*
Update csdp.cache.
Maxime Dénès
2016-07-08
|
*
Test file for #4858.
Maxime Dénès
2016-07-08
|
*
Add test file for #4880.
Maxime Dénès
2016-07-08
|
*
Update COPYRIGHT.
Maxime Dénès
2016-07-08
|
*
Merge remote-tracking branch 'github/pr/243' into v8.5
Maxime Dénès
2016-07-08
|
|
\
*
|
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-07-07
|
\
|
|
*
|
|
Merge remote-tracking branch 'github/bug4653' into v8.6
Matthieu Sozeau
2016-07-07
|
\
\
\
|
|
*
|
Prevent "Load" from displaying all the intermediate subgoals.
Guillaume Melquiond
2016-07-07
|
|
*
|
Do not display goals in -compile-verbose mode (bug #4841).
Guillaume Melquiond
2016-07-07
|
*
|
|
Do not use implicit type info for (x := t) bindings
Matthieu Sozeau
2016-07-07
*
|
|
|
Merge remote-tracking branch 'github/bug4873' into v8.6
Matthieu Sozeau
2016-07-07
|
\
\
\
\
|
*
|
|
|
Program: fix #4873: transparency option not used
Matthieu Sozeau
2016-07-07
|
/
/
/
/
|
|
*
|
Update csdp.cache.
Maxime Dénès
2016-07-06
|
|
*
|
Fix typo in configure (noticed by Jason).
Maxime Dénès
2016-07-06
*
|
|
|
Merge branch 'primproj' into v8.6
Matthieu Sozeau
2016-07-06
|
\
\
\
\
|
*
|
|
|
Fix reopened bug #3317.
Matthieu Sozeau
2016-07-06
|
*
|
|
|
Fixed bug #4622.
Matthieu Sozeau
2016-07-06
|
*
|
|
|
Disallow dependent case on prim records w/o eta
Matthieu Sozeau
2016-07-06
|
*
|
|
|
Renaming to more generic has_dependent_elim test
Matthieu Sozeau
2016-07-06
|
*
|
|
|
Move is_prim... to Inductiveops and correct Scheme
Matthieu Sozeau
2016-07-06
|
*
|
|
|
primproj: warning and avoid error.
Matthieu Sozeau
2016-07-06
|
/
/
/
/
|
|
|
*
improved complexity in nsatz
thery
2016-07-06
|
|
*
|
Merge remote-tracking branch 'github/pr/199' into v8.5
Maxime Dénès
2016-07-06
|
|
|
\
\
|
|
*
\
\
Merge remote-tracking branch 'github/pr/241' into v8.5
Maxime Dénès
2016-07-06
|
|
|
\
\
\
*
|
|
|
|
|
Fix #4793: Coq 8.6 should accept -compat 8.6
Maxime Dénès
2016-07-06
|
|
*
|
|
|
Bump version number in preparation for 8.5pl2 release.
Maxime Dénès
2016-07-06
|
*
|
|
|
|
Fix test-suite file 3690
Matthieu Sozeau
2016-07-06
|
|
*
|
|
|
Deduplicate some names in .mailmap
Jason Gross
2016-07-06
|
*
|
|
|
|
Univs: fix internalization of (x := T) and casts
Matthieu Sozeau
2016-07-06
|
/
/
/
/
/
|
*
|
|
|
Fix indentation of configure printout
Jason Gross
2016-07-06
[next]