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
*
Injection: do not fail when arguments have sort Prop.
Maxime Dénès
2014-04-29
*
Native compiler: hide compiled files in a .coq-native subdirectory.
Maxime Dénès
2014-04-29
*
Completing 5eb53b5bc8d765ed75e965f43f1084e18efc8790 (I unfortunately
Hugo Herbelin
2014-04-29
*
Reduce the amount of "Coq <" prompts generated by coq_tex. (Partial fix for b...
Guillaume Melquiond
2014-04-28
*
Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)
Guillaume Melquiond
2014-04-28
*
Recognize Parameters as a command in coqdoc. (Fix for bug #3279)
Guillaume Melquiond
2014-04-28
*
Mark lazymatch as an Ltac keyword for coqdoc. (Fix for bug #3276)
Guillaume Melquiond
2014-04-28
*
Remove unused lookup table.
Guillaume Melquiond
2014-04-28
*
Fix broken commit 2bcb2cb.
Guillaume Melquiond
2014-04-28
*
Fix incorrect syntax highlighting after the Goal command.
Guillaume Melquiond
2014-04-28
*
Fixing coqdoc bug #3292 (unfortunate collision betweens the relative
Hugo Herbelin
2014-04-28
*
Fixing #3293 (eta-expansion at "match" printing time was failing
Hugo Herbelin
2014-04-28
*
Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to
Hugo Herbelin
2014-04-28
*
Rewriting [lapply] tactic in the new monad.
Pierre-Marie Pédrot
2014-04-27
*
Giving true proof-terms in inversion instead of metas.
Pierre-Marie Pédrot
2014-04-27
*
coq_makefile: -I for the new stm/ dir
Enrico Tassi
2014-04-25
*
Adding a stm/ folder, as asked during last workgroup. It was essentially moving
Pierre-Marie Pédrot
2014-04-25
*
Removing Autoinstance once and for all.
Pierre-Marie Pédrot
2014-04-25
*
Removing useless try-with clauses in Goal.enter variants.
Pierre-Marie Pédrot
2014-04-25
*
Future: memory optimization when forcing a chained pure computation
Enrico Tassi
2014-04-25
*
Opaqueproofs: sink futures when interactive
Enrico Tassi
2014-04-25
*
print futures in caml toplevel too
Enrico Tassi
2014-04-25
*
Fix a second, trickier, typo in Termops.eta_reduce_head.
Arnaud Spiwack
2014-04-25
*
Adding a debug printer for futures.
Pierre-Marie Pédrot
2014-04-25
*
Fixing various backtrace recordings.
Pierre-Marie Pédrot
2014-04-25
*
Fix a small typo in Termops.eta_reduce_head.
Arnaud Spiwack
2014-04-25
*
Adding a [fold_map] operation on constrs.
Pierre-Marie Pédrot
2014-04-24
*
Writing tclABSTRACT in the new monad. In particular the unsafe status is now
Pierre-Marie Pédrot
2014-04-24
*
Better representation of evar filters: we represent the vacuous filters of
Pierre-Marie Pédrot
2014-04-23
*
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Pierre-Marie Pédrot
2014-04-23
*
Import proof of decidability of negated formulas from Coquelicot.
Guillaume Melquiond
2014-04-23
*
Remove some uses of excluded middle.
Guillaume Melquiond
2014-04-22
*
Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from Co...
Guillaume Melquiond
2014-04-22
*
Add regression tests for 3188 and 3265
Jason Gross
2014-04-22
*
Removing the compatibility layer from Leminv. Also removed an undocumented
Pierre-Marie Pédrot
2014-04-22
*
Using the new monad tactic in Inv.
Pierre-Marie Pédrot
2014-04-22
*
Removing tactic compatibility layer from Elim.
Pierre-Marie Pédrot
2014-04-22
*
Small code cleaning in Tacticals.
Pierre-Marie Pédrot
2014-04-22
*
Simplifying interface of elimination tactics. They used dummy clausenvs, and
Pierre-Marie Pédrot
2014-04-22
*
Adding a test for bug #2923.
Pierre-Marie Pédrot
2014-04-20
*
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
[next]