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
*
Modularization of BinPos + fixes in Stdlib
letouzey
2011-05-05
*
Definitions of positive, N, Z moved in Numbers/BinNums.v
letouzey
2011-05-05
*
Zdiv: results about eqm (the equality modulo some N) under a section
letouzey
2011-05-05
*
Better comments and organisation in Datatypes.v
letouzey
2011-05-05
*
Extraction: allow extraction foo when foo is an alias notation
letouzey
2011-05-05
*
Fix merge, Cumul moved to CUMUL
msozeau
2011-05-05
*
Merge branch 'subclasses' into coq-trunk
msozeau
2011-05-05
*
First phase removing obsolete support for eta up to conversion in
herbelin
2011-05-04
*
As many notation for for vectors as for List.
pboutill
2011-05-03
*
when -camlbin is explicitly given in configure, $OCAML* are $CAMLBIN/exec.
pboutill
2011-04-29
*
Fixed a bug causing inconsistent states during proof editting.
aspiwack
2011-04-29
*
Some comments.
aspiwack
2011-04-29
*
Typo in test InitSyntax.out
herbelin
2011-04-29
*
Choose relative directory over configured directory for coqlib.
pboutill
2011-04-29
*
Attempt to use more local doc in coqide
pboutill
2011-04-28
*
CHANGES update
pboutill
2011-04-28
*
coq_makefile big cleanup
pboutill
2011-04-28
*
coqtop -config returns coq returns coq environments at exection time
pboutill
2011-04-28
*
Revert r14078 "Partial backtrack on the support for open terms in destruct/in...
gmelquio
2011-04-28
*
Partial backtrack on the support for open terms in destruct/induction:
gmelquio
2011-04-28
*
Coqide: try to properly send interrupts to coqtop on Win32
letouzey
2011-04-28
*
Adding "Tactic Notation" in doc index.
herbelin
2011-04-28
*
Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixed
herbelin
2011-04-28
*
Fixed notation printing bug when curly brackets are involved (requests
herbelin
2011-04-28
*
Updating CHANGES
herbelin
2011-04-27
*
Fixing output of Notations2.v test messed up in r14060
herbelin
2011-04-27
*
Pcoq.ml4: fix a typo in a comment to please ocamldoc
letouzey
2011-04-26
*
G_vernac can be parsed without grammar.cma
letouzey
2011-04-26
*
dev/base_include: no more mod_self_id
letouzey
2011-04-26
*
Fixing commit r14061 (changes in file tactics.ml were mistakenly committed).
herbelin
2011-04-26
*
Coqide: fix remove_current_view_page (#2499)
letouzey
2011-04-26
*
Fix for handling of -R "" in coqdoc (bug #2423).
herbelin
2011-04-25
*
Fixing and completing interpretation of let's in notations for iterated binders.
herbelin
2011-04-25
*
Fixing and completing interpretation of let's in notations for iterated binders.
herbelin
2011-04-25
*
Yet another bug in printing fix with let-in binders
herbelin
2011-04-24
*
Fixing bug in printing let-in binders in fix/cofix
herbelin
2011-04-24
*
Fixed a bug of destruct which was sometimes forgetting local definitions behi...
herbelin
2011-04-24
*
Coqide: fix synchro when restarting during a single step
letouzey
2011-04-22
*
Coqide: let's try to be synchronuous when killing coqtop
letouzey
2011-04-21
*
Coqide: remove some dead code
letouzey
2011-04-21
*
Coqlib: avoid deadlock under win32 with force_reset_initial
letouzey
2011-04-21
*
Coqide: back to using Unix.stderr in create_process
letouzey
2011-04-21
*
Coqide: better handling of stdout/stderr in win32
letouzey
2011-04-21
*
Coqide: typo
letouzey
2011-04-21
*
Coqide: quote coqtop filename if necessary
letouzey
2011-04-21
*
Coqide: a special kill function for win32
letouzey
2011-04-21
*
Coqide: try to avoid displaying error messages on coqide's console
letouzey
2011-04-21
*
Coqide: better construction of default coqtop path
letouzey
2011-04-21
*
Win32: remove the need for Coq.bat and Coqide.bat
letouzey
2011-04-21
*
Win32: if we make coqide console-free, then stderr/stdout/sdtin shouldn't be ...
letouzey
2011-04-21
[next]