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
*
Parsing evar instances.
Hugo Herbelin
2014-09-12
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
No plural for only one non existing focused goal.
Hugo Herbelin
2014-09-12
*
Fix source of initial goal.
Hugo Herbelin
2014-09-12
*
Commit 682aa67cc80 about enforcing that apply does not create new
Hugo Herbelin
2014-09-12
*
Discontinued xml plugin: improve the README.
Arnaud Spiwack
2014-09-12
*
Replace the list of argument in tacexpr with a single row argument.
Arnaud Spiwack
2014-09-12
*
Oopps.. fixed the .ml not the .ml4
Matthieu Sozeau
2014-09-11
*
Use an AST for strategy names.
Matthieu Sozeau
2014-09-11
*
Fix test-suite files, and move some opened to closed.
Matthieu Sozeau
2014-09-11
*
Add a flag for restricting resolution of typeclasses to
Matthieu Sozeau
2014-09-11
*
Keeping a sub-optimal behavior of intros_possibly_replacing for compatibility...
Hugo Herbelin
2014-09-11
*
Other bugs with "inversion as" (collision between user-provided names and gen...
Hugo Herbelin
2014-09-11
*
Fix bug #3594: eta for constructors and functions at the same time which
Matthieu Sozeau
2014-09-11
*
Fix bug #3596, wrong treatment of projections in compute_constelim_direct.
Matthieu Sozeau
2014-09-11
*
Fix bug #3505.
Matthieu Sozeau
2014-09-11
*
Fixing bug #3605.
Pierre-Marie Pédrot
2014-09-11
*
Removing remaining documentation of the XML plugin.
Pierre-Marie Pédrot
2014-09-11
*
A step towards better differentiating when w_unify is used for subterm
Hugo Herbelin
2014-09-10
*
Parsing and printing of primitive projections, fix buggy behavior when
Matthieu Sozeau
2014-09-10
*
Fix generation of inductive elimination principle for primitive records.
Matthieu Sozeau
2014-09-10
*
Fix categorization of recursive inductives.
Matthieu Sozeau
2014-09-10
*
Fixing localisation of tactic errors (my mistake in himsg.ml essentially).
Hugo Herbelin
2014-09-10
*
More small bugs in intros_replacing.
Hugo Herbelin
2014-09-10
*
Fixing inversion after having fixed intros_replacing
Hugo Herbelin
2014-09-10
*
Example for apply and evars.
Hugo Herbelin
2014-09-10
*
Removing "eqn:" for "induction" in reference manual.
Hugo Herbelin
2014-09-10
*
VernacExtend does not dispatch on type anymore.
Pierre-Marie Pédrot
2014-09-10
*
- Fix printing and parsing of primitive projections, including the Set
Matthieu Sozeau
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
*
|
Displaying genarg tag in idtac.
Pierre-Marie Pédrot
2014-09-09
*
|
Installer for win improved
Enrico Tassi
2014-09-09
|
/
*
IDE: escape popup text (close: 3600)
Enrico Tassi
2014-09-09
*
Load Prelude.vi if not Prelude.vo is found (Close: 3595)
Enrico Tassi
2014-09-09
*
Marshalling errors should be bold and red (should never happen actually)
Enrico Tassi
2014-09-09
*
A marshalling failure does not make a worker `Old
Enrico Tassi
2014-09-09
*
Documenting the new Undo semantics
Enrico Tassi
2014-09-09
*
Back: print subgoals as in 8.4 (Close: 3585)
Enrico Tassi
2014-09-09
*
BackTo not part of the doc when used by emacs
Enrico Tassi
2014-09-09
*
Undo: if the ui is coqtop (command line) then Undo is not part of the doc.
Enrico Tassi
2014-09-09
*
Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407)
Enrico Tassi
2014-09-09
*
IDE: disable editable text area underline when -debug
Enrico Tassi
2014-09-09
*
toploop plugins taken into account when printing --help (close: 3535)
Enrico Tassi
2014-09-09
*
Installer for win32
Enrico Tassi
2014-09-09
[next]