index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
lib
Commit message (
Expand
)
Author
Age
*
When loading libraries, feed back dependencies.
Carst Tankink
2014-10-13
*
STM: primitives to snapshot a .vi while in interactive mode
Enrico Tassi
2014-10-13
*
library/opaqueTables: enable their use in interactive mode
Enrico Tassi
2014-10-13
*
Fixup leading ./ path cleaning
Pierre Boutillier
2014-10-09
*
Splitting out of auto.ml a file hints.ml dedicated to hints so as to
Hugo Herbelin
2014-10-07
*
A few improvements on pattern-matching compilation.
Hugo Herbelin
2014-10-05
*
STM: report the (structured) goals as XML
Carst Tankink
2014-10-01
*
Remove some 'deprecated' warnings.
Xavier Clerc
2014-09-25
*
Fix debug printing with primitive projections.
Matthieu Sozeau
2014-09-18
*
Undo prints only if coqtop || emacs
Enrico Tassi
2014-09-16
*
Undo: if the ui is coqtop (command line) then Undo is not part of the doc.
Enrico Tassi
2014-09-09
*
toploop plugins taken into account when printing --help (close: 3535)
Enrico Tassi
2014-09-09
*
Removing dead code relative to the XML plugin.
Pierre-Marie Pédrot
2014-09-08
*
Adding a Ftactic module for potentially focussing tactics.
Pierre-Marie Pédrot
2014-09-05
*
coqworkmgr
Enrico Tassi
2014-09-02
*
Type-safe version of genarg list / pair / opt functions.
Pierre-Marie Pédrot
2014-08-29
*
Simplification of Genarg unpackers.
Pierre-Marie Pédrot
2014-08-29
*
Fixing bug #3541.
Pierre-Marie Pédrot
2014-08-28
*
"allows to", like "allowing to", is improper
Jason Gross
2014-08-25
*
STM: new "par:" goal selector, like "all:" but in parallel
Enrico Tassi
2014-08-05
*
STM: code restructured to reuse task queue for tactics
Enrico Tassi
2014-08-05
*
STM: encapsulate Pp.message in Feedback.feedback
Carst Tankink
2014-08-04
*
Removing the call to Weak.get_copy in hashsets.
Pierre-Marie Pédrot
2014-07-31
*
Improve intersection of regular trees.
Maxime Dénès
2014-07-31
*
Pp: only one default feedback id
Enrico Tassi
2014-07-29
*
Pp compiles after feedback
Enrico Tassi
2014-07-29
*
Revert "Adding a "is_val" primitive to IStream."
Pierre-Marie Pédrot
2014-07-24
*
Refine check_is_subterm.
Maxime Dénès
2014-07-22
*
Made intersection on regular trees less intensional.
Maxime Dénès
2014-07-22
*
Refining match subterm and commutative cut rules. The parameters that are
Maxime Dénès
2014-07-22
*
Adding a "is_val" primitive to IStream.
Pierre-Marie Pédrot
2014-07-22
*
Universe level maps use HMaps.
Pierre-Marie Pédrot
2014-07-21
*
Missing primitives in HMap.
Pierre-Marie Pédrot
2014-07-21
*
Fixing semantics of HSet.inter and HSet.diff.
Pierre-Marie Pédrot
2014-07-21
*
Adding a "time" tactical for benchmarking purposes. In case the tactic
Hugo Herbelin
2014-07-13
*
An outdated comment + comment layout.
Arnaud Spiwack
2014-07-11
*
STM: let toploop plugins specify the flags for STM workers
Enrico Tassi
2014-07-11
*
STM: flag to turn off branch reopening
Enrico Tassi
2014-07-11
*
Feedback: LoadedFile + Goals
Enrico Tassi
2014-07-11
*
make the standard logging facility stm aware
Enrico Tassi
2014-07-11
*
option to always delegate futures to workers
Enrico Tassi
2014-07-10
*
more APIs in TQueue and CThread
Enrico Tassi
2014-07-10
*
check_for_interrupt: better (but slower) in threading mode
Enrico Tassi
2014-07-10
*
Revert "time tac" (committed by mistake).
Hugo Herbelin
2014-07-07
*
time tac
Hugo Herbelin
2014-07-07
*
Adding a coiterator to IStream.
Pierre-Marie Pédrot
2014-07-03
*
all coqide specific files moved into ide/
Enrico Tassi
2014-06-25
*
Less ocaml warnings.
Hugo Herbelin
2014-06-21
*
Deprecate useless option -quality.
Guillaume Melquiond
2014-06-13
*
Deprecate useless option -unsafe.
Guillaume Melquiond
2014-06-13
[next]