index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
dev
Age
Commit message (
Expand
)
Author
2015-11-18
MacOS package script: do not fail if link to /Applications already exists.
Maxime Dénès
2015-11-16
Being more precise and faithful about the origin of the file reporting
Hugo Herbelin
2015-11-13
MacOS package script: do not fail if directory _dmg already exists.
Maxime Dénès
2015-11-12
Script building MacOS package.
Maxime Dénès
2015-10-29
Fixing another instance of bug #3267 in eauto, this time in the
Hugo Herbelin
2015-10-28
Refine Gregory Malecha's patch on VM and universe polymorphism.
Maxime Dénès
2015-10-28
Adds support for the virtual machine to perform reduction of universe polymor...
Gregory Malecha
2015-10-14
Reverting modifications in dev/top_printers pushed mistakenly.
Pierre-Marie Pédrot
2015-10-14
Fixing perfomance issue of auto hints induced by universes.
Pierre-Marie Pédrot
2015-10-13
Fix some typos.
Guillaume Melquiond
2015-10-09
Code cleaning in VM (with Benjamin).
Maxime Dénès
2015-10-09
Minor typo in universe polymorphism doc.
Maxime Dénès
2015-10-02
Updating versions history with data from Gérard.
Hugo Herbelin
2015-10-02
Update the history of versions with recent versions.
Hugo Herbelin
2015-10-02
Univs: More info for developers.
Matthieu Sozeau
2015-09-17
Fix Windows installer.
Guillaume Melquiond
2015-08-17
windows build scripts made more accurate in detecting failures
Enrico Tassi
2015-07-30
A printer for printing constants of the env (maybe useful when there are not ...
Hugo Herbelin
2015-07-23
adding a missing case for printing zippers.
Gregory Malecha
2015-06-29
Assumptions: more informative print for False axiom (Close: #4054)
Enrico Tassi
2015-06-29
win: compile with -debug
Enrico Tassi
2015-06-25
Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.
Thomas Sibut-Pinote
2015-06-01
script to build 64 coq installer for windows
Enrico Tassi
2015-04-21
Fixing #4198 (looking for subterms also in the return clause of match).
Hugo Herbelin
2015-03-27
use a more compact representation of non-constant constructors
Benjamin Gregoire
2015-03-26
fix compilation
Benjamin Gregoire
2015-02-19
Adding a possible DEPRECATED flag to VERNAC EXTEND statements.
Pierre-Marie Pédrot
2015-02-12
Revert "Using same code for browsing physical directories in coqtop and coqdep."
Hugo Herbelin
2015-02-12
Using same code for browsing physical directories in coqtop and coqdep.
Hugo Herbelin
2015-02-05
Windows installer cleanup
Enrico Tassi
2015-02-02
Removing dead code.
Pierre-Marie Pédrot
2015-01-17
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-15
vm_printers: fix compilation
Enrico Tassi
2015-01-12
Update headers.
Maxime Dénès
2015-01-08
Avoiding introducing yet another convention in naming files.
Hugo Herbelin
2014-12-30
Compatibility ocaml 3.12.
Hugo Herbelin
2014-12-30
Minor fixes for the win32 installer
Enrico Tassi
2014-12-19
Win32: fix installer
Enrico Tassi
2014-12-16
More printers for ltac signatures.
Hugo Herbelin
2014-12-09
Switch the few remaining iso-latin-1 files to utf8
Pierre Letouzey
2014-12-07
Removing import of Proofview in debugger because its module Goal hides
Hugo Herbelin
2014-12-05
More printers in tracer.
Hugo Herbelin
2014-12-04
Reactivating option "Set Printing Existential Instances" for asking printing ...
Hugo Herbelin
2014-11-27
Reverting the following block of three commits:
Hugo Herbelin
2014-11-26
Experimenting always forcing convertibility on strict implicit arguments
Hugo Herbelin
2014-11-23
Add printer for transparent state for ocamldebug.
Hugo Herbelin
2014-11-22
Specific printer of Evar.Set.t for ocamldebug + more information in
Hugo Herbelin
2014-11-15
Adding a pretty-printing style library.
Pierre-Marie Pédrot
2014-11-10
Plug the dynamic tags in the Richpp mechanism.
Pierre-Marie Pédrot
2014-10-31
More "open" by default for trace debugging.
Hugo Herbelin
[next]