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
...
*
Adding a test for bug #3285.
Pierre-Marie Pédrot
2014-04-20
*
Fixing bug #3285.
Pierre-Marie Pédrot
2014-04-20
*
Adding a [map] primitive to the tactic monad. Hopefully this should be
Pierre-Marie Pédrot
2014-04-20
*
Fixing missing headers.
Hugo Herbelin
2014-04-16
*
Closing bug #3260
Julien Forest
2014-04-14
*
Fix guard condition for nested cofixpoints in checker.
Maxime Dénès
2014-04-10
*
Fix guard condition for nested cofixpoints.
Maxime Dénès
2014-04-10
*
better description of bug 3251
Enrico Tassi
2014-04-10
*
Have the feedback bus as a backend for dumping globs.
Carst Tankink
2014-04-10
*
Dumpglob: factor out reference dumping.
Carst Tankink
2014-04-10
*
CoqIDE: options for syntax highlighting
Enrico Tassi
2014-04-10
*
CoqIDE: removing a timer may raise an exception
Enrico Tassi
2014-04-10
*
coqtop -batch refuses Back 1 but accepts Undo.
Pierre Boutillier
2014-04-10
*
By resolution of the CoqWG, instantiate must not be used now that refine works
Pierre Boutillier
2014-04-10
*
No more Coersion in Init.
Pierre Boutillier
2014-04-10
*
Define [projT3] and [proj3_sig]
Jason Gross
2014-04-10
*
Test case for bug 3037
Jason Gross
2014-04-10
*
Test case for 3164
Jason Gross
2014-04-10
*
Test case for bug 3262
Jason Gross
2014-04-10
*
Test case for bug #3217
Jason Gross
2014-04-10
*
Add a regression test for bug 3001
Jason Gross
2014-04-10
*
Add another critical bug to the test-suite.
Maxime Dénès
2014-04-09
*
Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with...
Pierre Boutillier
2014-04-09
*
Adapt coq_makefile build rules to new -R -I semantic
Pierre Boutillier
2014-04-09
*
Adapt test-suite to -I is ML only
Pierre Boutillier
2014-04-09
*
Fix exponential behavior in native compiler with retroknowledge.
Maxime Dénès
2014-04-09
*
Fix name of some Int31 operations in native compiler.
Maxime Dénès
2014-04-09
*
Removing handshake from Spawn. It used marshalling, which is bad for
Pierre-Marie Pédrot
2014-04-09
*
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
[prev]
[next]