index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2012-01-19
Pretty printing of generalized binder
pboutill
2012-01-19
Boolean Option Patterns Compatibility
pboutill
2012-01-19
No more use of tauto in Init/
pboutill
2012-01-17
Fixed the pretty-printing of the Program plugin.
ppedrot
2012-01-17
Makefile: fix make distclean w.r.t. test-suite
letouzey
2012-01-17
MSetAVL: better implementation of filter suggested by X. Leroy
letouzey
2012-01-17
Some fix in beautify pretty-printer
pboutill
2012-01-16
Parameters in pattern first step.
pboutill
2012-01-16
Inductiveops.nb_*{,_env} cleaning
pboutill
2012-01-16
Bug 2679: Do not try to install cmxs with -byte-only
pboutill
2012-01-16
Bug 2676: ./configure --prefix shoudn't ask for a config directory.
pboutill
2012-01-16
make mli-doc fix
pboutill
2012-01-14
coq_micromega.ml: fix order of recursive calls to rconstant
glondu
2012-01-14
Add distclean back to test-suite/Makefile
glondu
2012-01-14
More newlines in debugging output of psatzl
glondu
2012-01-13
Added a Btauto plugin, that solves boolean tautologies.
ppedrot
2012-01-13
Added the decidability of (<=) on nat.
ppedrot
2012-01-12
Fix typo
glondu
2012-01-10
Fix printing of instances, generalized arguments.
msozeau
2012-01-07
Fix typo
glondu
2012-01-06
Fixed the itarget of the previous commit...
ppedrot
2012-01-06
Added a typeclass-based system to reason on decidable propositions.
ppedrot
2012-01-06
Forbids (as it has always been the behaviour) to have two different open
aspiwack
2012-01-06
Fixes bug #2654 (tactic instantiate failing to update existential variables).
aspiwack
2012-01-05
Backtracking on r14876 (fix for bug #2267): extra scopes might be
herbelin
2012-01-04
Fixing Arguments Scope bug when too many scopes are given (bug #2667).
herbelin
2012-01-04
Type inference unification: fixed a 8.4 bug in the presence of unification
herbelin
2012-01-03
Makefile.doc: attempt to solve race condition for creating doc/refman/html.
herbelin
2011-12-27
Bug 2669 and more: make full-stdlib
pboutill
2011-12-26
Coqdoc: Fixing missing newline when using "Proof term."
herbelin
2011-12-26
Reference Manual: misc fixes (spelling, index, updating pre-8.0 syntax).
herbelin
2011-12-26
update CHANGES w.r.t. simpl
gareuselesinge
2011-12-25
Version number, copyright, credits: missing updates.
herbelin
2011-12-23
Credits for 8.4: More exhaustive list of external contributors.
herbelin
2011-12-23
myocamlbuild: -DWIN32 instead of -DWin32
letouzey
2011-12-23
Configure: the backslashes in win32 paths should be escaped
letouzey
2011-12-22
Credits for 8.4 + resetting COMPATIBILITY file.
herbelin
2011-12-21
sequel of previous commit
letouzey
2011-12-21
Isolate a few types of Goptions in a pure .mli, solving a dep issue with ocam...
letouzey
2011-12-21
Pure interfaces shouldn't be mentionned in .mllib
letouzey
2011-12-21
adapt myocamlbuild after changes in coqdep_boot (.beautify)
letouzey
2011-12-21
Cleaning CHANGES file.
herbelin
2011-12-19
Notifying removal of accidental unfolding of recursive calls of
herbelin
2011-12-19
Arguments: check rename even if no implicit is specified
gareuselesinge
2011-12-19
test suite update after r14808
pboutill
2011-12-19
Bug 2377 part 2: old revision file is erased by install
pboutill
2011-12-19
Fixed some printing details for dependent evars in emacs mode. Patch
courtieu
2011-12-18
Granted legitimate wish #2607 (not exposing crude fixpoint body of
herbelin
2011-12-18
CoqIde files position is freedesktop compliant.
pboutill
2011-12-18
./configure & freedesktop
pboutill
[next]