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
...
*
nanoPG: when the cursor moves, scroll to make it appear on screen
Enrico Tassi
2014-04-09
*
nanoPG: takeover keypress only when text view has focus
Enrico Tassi
2014-04-09
*
Optimizing Int31 support in native compiler, by not tagging
Maxime Dénès
2014-04-09
*
Int31 decompilation in native compiler was still partial. Now fixed.
Maxime Dénès
2014-04-09
*
Machine arithmetic operations for native compiler.
Maxime Dénès
2014-04-09
*
Readback for int31 values from native compiler.
Maxime Dénès
2014-04-09
*
Full support for int31 values in native compiler.
Maxime Dénès
2014-04-09
*
Partial support for open terms in int31.
Maxime Dénès
2014-04-09
*
Had to split Nativelambda in two files because of Retroknowledge
Maxime Dénès
2014-04-09
*
Int31 literals in native compiler.
Maxime Dénès
2014-04-09
*
Uint31 support.
Maxime Dénès
2014-04-09
*
Add an option -Q (tentative name).
Guillaume Melquiond
2014-04-08
*
Fix universe handling (bug introduced in vi2vo commit)
Enrico Tassi
2014-04-08
*
printer for coqchk
Enrico Tassi
2014-04-08
*
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
[prev]
[next]