index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
dev
Commit message (
Expand
)
Author
Age
*
win32: embed NSIS for plugin writers
Enrico Tassi
2014-09-19
*
Fix debug printing with primitive projections.
Matthieu Sozeau
2014-09-18
*
win32: remove outdated splash screen
Enrico Tassi
2014-09-17
*
win32: use subsystem windows on windows (and not console)
Enrico Tassi
2014-09-17
*
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-12
*
VernacExtend does not dispatch on type anymore.
Pierre-Marie Pédrot
2014-09-10
*
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-09-09
*
Debug RAKAM
Pierre Boutillier
2014-08-26
*
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-18
*
STM: encapsulate Pp.message in Feedback.feedback
Carst Tankink
2014-08-04
*
A tentative uniform naming policy in module Inductiveops.
Hugo Herbelin
2014-08-01
*
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-28
*
all coqide specific files moved into ide/
Enrico Tassi
2014-06-25
*
Dummy commit to test the new setup of coq-commits mailinglist (bis)
Pierre Letouzey
2014-06-17
*
Dummy commit to test the new setup of coq-commits mailinglist
Pierre Letouzey
2014-06-17
*
Change Ltac constr matching semantics to consider universes when merging two
Matthieu Sozeau
2014-06-15
*
- Fix bug #3368, due to wrong use of the Cst_stack for projections.
Matthieu Sozeau
2014-06-11
*
Fix module order in printers.mllib
Matthieu Sozeau
2014-06-10
*
Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...
Matthieu Sozeau
2014-06-10
*
Moving a Thread.yield in check_interrupt.
Pierre-Marie Pédrot
2014-06-07
*
Adding a new Control file centralizing the control options of Coq.
Pierre-Marie Pédrot
2014-06-07
*
A little bit of documentation about V5.10 and V6.3 and V7.
Hugo Herbelin
2014-06-01
*
- Fix in kernel conversion not folding the universe constraints
Matthieu Sozeau
2014-05-26
*
Isolating a function "make_abstraction", new name of "letin_abstract",
Hugo Herbelin
2014-05-08
*
Renaming new_induct -> induction; new_destruct -> destruct.
Hugo Herbelin
2014-05-08
*
Moving Dnet-related code to tactics/.
Pierre-Marie Pédrot
2014-05-08
*
Remove Lemmas from base_include, it's not linked in dev/printers anymore
Matthieu Sozeau
2014-05-06
*
Cleanup before merge with the trunk
Matthieu Sozeau
2014-05-06
*
Add incompatibilities paragraph in doc about universe polymorphism.
Matthieu Sozeau
2014-05-06
*
Add doc on the new API for universe polymorphism and primitive projections
Matthieu Sozeau
2014-05-06
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
Fix issue #88: restrict_universe_context was wrongly forgetting about constra...
Matthieu Sozeau
2014-05-06
*
'Pretty' printer for wf_paths
Pierre
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
print futures in caml toplevel too
Enrico Tassi
2014-04-25
*
Adding a debug printer for futures.
Pierre-Marie Pédrot
2014-04-25
[next]