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
*
Get rid of messages "emitting ..." when compiling .v files
Pierre Letouzey
2013-12-16
*
A few fixes to the build system (mostly for ocamlbuild)
Pierre Letouzey
2013-12-16
*
Added test-suite for bug #2990.
Pierre-Marie Pédrot
2013-12-16
*
Dedicated inductive for return values of rewrite strategies.
Pierre-Marie Pédrot
2013-12-16
*
Do not overallocate closures' named environments in infos. Modifying the access
Pierre-Marie Pédrot
2013-12-15
*
Do not compile coqide with -thread
Pierre Boutillier
2013-12-12
*
Patch for supporting [From Xxx Require Yyy Zzz.]
Gregory Malecha
2013-12-12
*
Better unification for [projT1] and [proj1_sig].
Jason Gross
2013-12-12
*
Generalize eq_proofs_unicity
Jason Gross
2013-12-12
*
Documenting the tactic-in-term construction.
Pierre-Marie Pédrot
2013-12-11
*
Fix CoqIDE compilation under standard version of lablgtk2
Enrico Tassi
2013-12-11
*
Fixing backtrace registering of various tactic-related try-with blocks.
Pierre-Marie Pédrot
2013-12-11
*
Fix CoqIDE on windows
Enrico Tassi
2013-12-10
*
Renaming elisp files to avoid conflict with pg in distribs.
Pierre Courtieu
2013-12-10
*
Fix printing of Ltac's backtrace.
Arnaud Spiwack
2013-12-09
*
Stylistic change.
Arnaud Spiwack
2013-12-09
*
Fix test-suite/success/evars.v.
Arnaud Spiwack
2013-12-06
*
Remove duplicate test-suite file.
Arnaud Spiwack
2013-12-06
*
Fix the refine related test-suite files to account for the new refine.
Arnaud Spiwack
2013-12-06
*
Missing file in commit 1fb883.
Arnaud Spiwack
2013-12-06
*
Fix g_derive.ml4.
Arnaud Spiwack
2013-12-04
*
Documentation of the Derive plugin.
Arnaud Spiwack
2013-12-04
*
Stm: remove an assertion.
Arnaud Spiwack
2013-12-04
*
Derive plugin.
Arnaud Spiwack
2013-12-04
*
Fix Admitted.
Arnaud Spiwack
2013-12-04
*
Proof_global: fix start_proof comment after the preceding commits.
Arnaud Spiwack
2013-12-04
*
Factoring(continued).
Arnaud Spiwack
2013-12-04
*
Refactoring: storing more information in the terminator closure.
Arnaud Spiwack
2013-12-04
*
The commands that initiate proofs are now in charge of what happens when proo...
Arnaud Spiwack
2013-12-04
*
Vernac classification: allow for commands which start proofs but must be sync...
Arnaud Spiwack
2013-12-04
*
Allow proofs to start with dependent goals.
Arnaud Spiwack
2013-12-04
*
Improved the presentation of the proof of UIP_refl_nat.
Hugo Herbelin
2013-12-04
*
Add lemma derivable_pt_lim_atan.
Guillaume Melquiond
2013-12-04
*
Removing useless meta-related functions.
Pierre-Marie Pédrot
2013-12-03
*
Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.
Guillaume Melquiond
2013-12-03
*
Silence some warning about references in documentation.
Guillaume Melquiond
2013-12-03
*
Remove a useless hypothesis from Rle_Rinv.
Guillaume Melquiond
2013-12-03
*
Ensure locality modifiers are properly highlighted in CoqIDE.
Guillaume Melquiond
2013-12-03
*
Silence compilation warning by avoiding some deprecated constructs.
Guillaume Melquiond
2013-12-03
*
Test case for bug#2848.
xclerc
2013-12-02
*
Porting type interpretation in Tacinterp to the new tactics.
Pierre-Marie Pédrot
2013-12-02
*
Writing [cut] tactic using the new monad.
Pierre-Marie Pédrot
2013-12-02
*
Test suite: update output reference.
xclerc
2013-12-02
*
Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr//gitroot/coq/coq into t...
xclerc
2013-12-02
|
\
*
|
Print logical name rather than path (thus allowing reproducible tests).
xclerc
2013-12-02
|
*
Removing RefArgType generic argument.
Pierre-Marie Pédrot
2013-12-01
|
*
Ensuring the right parsing of glob arguments, used by refine
Pierre-Marie Pédrot
2013-12-01
|
*
Fixing ltac constr variable handling in refine.
Pierre-Marie Pédrot
2013-11-30
|
*
Adding printing of ltac envs to debugger.
Pierre-Marie Pédrot
2013-11-30
|
*
Getting rid of casted_open_constr. It was only used by the
Pierre-Marie Pédrot
2013-11-30
[next]