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
*
Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. (Fi...
Guillaume Melquiond
2014-04-07
*
Allowing proof view to be detached in CoqIDE.
Pierre-Marie Pédrot
2014-04-07
*
Transfering the initial goals from the proofview to the proof object.
Pierre-Marie Pédrot
2014-04-07
*
Removing unused functions in Refiner.
Pierre-Marie Pédrot
2014-04-06
*
Actually using the [modify] primitive.
Pierre-Marie Pédrot
2014-04-06
*
Adding an [modify] function to the tactic monad. It allows to modify
Pierre-Marie Pédrot
2014-04-06
*
Add tool for fully qualifying Require statements.
Guillaume Melquiond
2014-04-06
*
Change handling of loadpath and mlpath.
Guillaume Melquiond
2014-04-06
*
Completing text of the question on conservativity of CIC over CC (bug #2697).
Hugo Herbelin
2014-04-05
*
Test for bug #3142, actually duplicate of #3262.
Hugo Herbelin
2014-04-05
*
Fixing bug #3228 (fixing precedence of ltac variables over variables in env).
Hugo Herbelin
2014-04-05
*
Printers for ltac environments.
Hugo Herbelin
2014-04-05
*
closing bug 3037
Julien Forest
2014-04-05
*
Fix for bug #3107.
Guillaume Melquiond
2014-04-04
*
fixing Function doc
Julien Forest
2014-04-04
*
Recognize "Instance" in coqwc. (Fix for bug #2551)
Guillaume Melquiond
2014-04-04
*
Closing bug #3164
Julien Forest
2014-04-04
*
Prevent verbatim text from leaking out of comments. (See bug #2882)
Guillaume Melquiond
2014-04-04
*
Fixing coqchk. It was my fault, I misused canonical and user equalities
Pierre-Marie Pédrot
2014-04-04
*
Fixing #3262 which revealed a non-progressing, hence looping,
Hugo Herbelin
2014-04-04
*
Support other forms of "Proof" in coqwc. (Fix for bug #2735)
Guillaume Melquiond
2014-04-04
*
Remove option -g as it is non-portable yet does not have any effect on the te...
Guillaume Melquiond
2014-04-04
*
Clean up the .merlin
Thomas Refis
2014-04-03
*
A debug printer for Evd.Filter.t
Pierre Boutillier
2014-04-02
*
Add a test case for bug 3251
Jason Gross
2014-04-02
*
STM: be more resilient to explicit Back + Sideff commands (closes: 3251)
Enrico Tassi
2014-04-02
*
Fix Bug 3131 + Really drop mentions of info in refman.
Pierre Boutillier
2014-04-02
*
Fix Bug 3217
Pierre Boutillier
2014-04-02
*
Better error message when found more than once object of name ...
Pierre Boutillier
2014-04-02
*
Evars introduced by Proofview refining are flagged as GoalEvar. For some
Pierre-Marie Pédrot
2014-04-01
*
Updated debugging printers
Hugo Herbelin
2014-04-01
*
Propagating conversion_problem towards (postponed) evar/evar problems.
Hugo Herbelin
2014-04-01
*
Fixing bug #2900 (evar/evar unif was supposed to be treated in
Hugo Herbelin
2014-04-01
*
Removing the Change_evar refiner rule.
Pierre-Marie Pédrot
2014-03-31
*
Removing dead code in Tactics.
Pierre-Marie Pédrot
2014-03-31
*
Using the new refine interface to define ML tactics.
Pierre-Marie Pédrot
2014-03-28
*
Lighter interface for creating refining tactics.
Pierre-Marie Pédrot
2014-03-28
*
Newline on -slash warning in coqdep.
Pierre-Marie Pédrot
2014-03-28
*
Define Tactics.bring_hyps in the new monad.
Pierre-Marie Pédrot
2014-03-28
*
Removing tactic compatibility layer from Eqdecide.
Pierre-Marie Pédrot
2014-03-27
*
Cosmetic changes in Equality.
Pierre-Marie Pédrot
2014-03-27
*
Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.
Pierre-Marie Pédrot
2014-03-26
*
Removing Tacmach compatibility layer in Equality.
Pierre-Marie Pédrot
2014-03-26
*
Removing tactic compatibility layer in Equality.
Pierre-Marie Pédrot
2014-03-26
*
Removing Tacmach compatibility layer in Inv.
Pierre-Marie Pédrot
2014-03-26
*
Removing tactic compatibility layer from Inv.
Pierre-Marie Pédrot
2014-03-26
*
STM: when an error occurs in a worker send back a bunch of states
Enrico Tassi
2014-03-26
*
CoqIDE: better error reporting for Qed on incomplete proof
Enrico Tassi
2014-03-26
*
test for apply + TC resolution
Enrico Tassi
2014-03-26
*
Adding an interface to Eqdecide and putting the grammar rules in a dedicated
Pierre-Marie Pédrot
2014-03-26
[next]