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
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
2014-10-22
Split [Proofview] into a file where the basic operations on the state are def...
Arnaud Spiwack
2014-10-15
Fix ill-typed debugging function
Matthieu Sozeau
2014-10-13
Adding printers for ppproofview.
Hugo Herbelin
2014-10-10
Add debug printers for projections, fix printing of evar constraints
Matthieu Sozeau
2014-10-09
Adding printer for named_context_val and Goal.goal in debugger.
Hugo Herbelin
2014-10-07
Adding a printer for hints.
Hugo Herbelin
2014-10-02
Fixing interpretation of constr under binders which was broken after
Hugo Herbelin
2014-10-01
Fixing nice printing of error reporting with ml tactics bound to ltac names.
Hugo Herbelin
2014-10-01
Fixing use of arguments renaming in apply which was broken after
Hugo Herbelin
2014-09-27
Index keys instead of simply global references.
Matthieu Sozeau
2014-09-27
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-19
win32: embed NSIS for plugin writers
Enrico Tassi
2014-09-18
Fix debug printing with primitive projections.
Matthieu Sozeau
2014-09-17
win32: remove outdated splash screen
Enrico Tassi
2014-09-17
win32: use subsystem windows on windows (and not console)
Enrico Tassi
2014-09-12
Fix base_include due to change in argument order of env and evar_map
Matthieu Sozeau
2014-09-12
Uniformisation of the order of arguments env and sigma.
Hugo Herbelin
2014-09-12
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-10
VernacExtend does not dispatch on type anymore.
Pierre-Marie Pédrot
2014-09-09
Merge remote-tracking branch 'jason/win32-improvements' into trunk
Enrico Tassi
2014-09-09
Bump CoqSDK revision number
Jason Gross
2014-09-09
Add a VERBOSE flag to make-sdk-win32
Jason Gross
2014-09-09
Minor code style cleanup in make-sdk-win32
Jason Gross
2014-09-09
Support 64-bit cygwin
Jason Gross
2014-09-09
Support machines that have a full or nonexistant C drive
Jason Gross
2014-09-09
Support environments where `find` is Windows' find
Jason Gross
2014-09-09
Installer for win improved
Enrico Tassi
2014-09-09
Installer for win32
Enrico Tassi
2014-08-26
Debug RAKAM
Pierre Boutillier
2014-08-18
A reorganization of the "assert" tactics (hopefully uniform naming
Hugo Herbelin
2014-08-18
Reorganisation of intropattern code
Hugo Herbelin
2014-08-18
Fixing include of debugger.
Pierre-Marie Pédrot
2014-08-04
STM: encapsulate Pp.message in Feedback.feedback
Carst Tankink
2014-08-01
A tentative uniform naming policy in module Inductiveops.
Hugo Herbelin
2014-06-28
Moved code for finding subterms (pattern, induction, set, generalize, ...)
Hugo Herbelin
2014-06-28
Made the subterm finding function make_abstraction independent of the
Hugo Herbelin
2014-06-28
More open in base_include
Hugo Herbelin
2014-06-25
all coqide specific files moved into ide/
Enrico Tassi
2014-06-17
Dummy commit to test the new setup of coq-commits mailinglist (bis)
Pierre Letouzey
[next]