aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Expand)AuthorAge
* When loading libraries, feed back dependencies.Gravatar Carst Tankink2014-10-13
* STM: primitives to snapshot a .vi while in interactive modeGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Fixup leading ./ path cleaningGravatar Pierre Boutillier2014-10-09
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
* A few improvements on pattern-matching compilation.Gravatar Hugo Herbelin2014-10-05
* STM: report the (structured) goals as XMLGravatar Carst Tankink2014-10-01
* Remove some 'deprecated' warnings.Gravatar Xavier Clerc2014-09-25
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
* Undo prints only if coqtop || emacsGravatar Enrico Tassi2014-09-16
* Undo: if the ui is coqtop (command line) then Undo is not part of the doc.Gravatar Enrico Tassi2014-09-09
* toploop plugins taken into account when printing --help (close: 3535)Gravatar Enrico Tassi2014-09-09
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Adding a Ftactic module for potentially focussing tactics.Gravatar Pierre-Marie Pédrot2014-09-05
* coqworkmgrGravatar Enrico Tassi2014-09-02
* Type-safe version of genarg list / pair / opt functions.Gravatar Pierre-Marie Pédrot2014-08-29
* Simplification of Genarg unpackers.Gravatar Pierre-Marie Pédrot2014-08-29
* Fixing bug #3541.Gravatar Pierre-Marie Pédrot2014-08-28
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
* STM: code restructured to reuse task queue for tacticsGravatar Enrico Tassi2014-08-05
* STM: encapsulate Pp.message in Feedback.feedbackGravatar Carst Tankink2014-08-04
* Removing the call to Weak.get_copy in hashsets.Gravatar Pierre-Marie Pédrot2014-07-31
* Improve intersection of regular trees.Gravatar Maxime Dénès2014-07-31
* Pp: only one default feedback idGravatar Enrico Tassi2014-07-29
* Pp compiles after feedbackGravatar Enrico Tassi2014-07-29
* Revert "Adding a "is_val" primitive to IStream."Gravatar Pierre-Marie Pédrot2014-07-24
* Refine check_is_subterm.Gravatar Maxime Dénès2014-07-22
* Made intersection on regular trees less intensional.Gravatar Maxime Dénès2014-07-22
* Refining match subterm and commutative cut rules. The parameters that areGravatar Maxime Dénès2014-07-22
* Adding a "is_val" primitive to IStream.Gravatar Pierre-Marie Pédrot2014-07-22
* Universe level maps use HMaps.Gravatar Pierre-Marie Pédrot2014-07-21
* Missing primitives in HMap.Gravatar Pierre-Marie Pédrot2014-07-21
* Fixing semantics of HSet.inter and HSet.diff.Gravatar Pierre-Marie Pédrot2014-07-21
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
* An outdated comment + comment layout.Gravatar Arnaud Spiwack2014-07-11
* STM: let toploop plugins specify the flags for STM workersGravatar Enrico Tassi2014-07-11
* STM: flag to turn off branch reopeningGravatar Enrico Tassi2014-07-11
* Feedback: LoadedFile + GoalsGravatar Enrico Tassi2014-07-11
* make the standard logging facility stm awareGravatar Enrico Tassi2014-07-11
* option to always delegate futures to workersGravatar Enrico Tassi2014-07-10
* more APIs in TQueue and CThreadGravatar Enrico Tassi2014-07-10
* check_for_interrupt: better (but slower) in threading modeGravatar Enrico Tassi2014-07-10
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
* time tacGravatar Hugo Herbelin2014-07-07
* Adding a coiterator to IStream.Gravatar Pierre-Marie Pédrot2014-07-03
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* Less ocaml warnings.Gravatar Hugo Herbelin2014-06-21
* Deprecate useless option -quality.Gravatar Guillaume Melquiond2014-06-13
* Deprecate useless option -unsafe.Gravatar Guillaume Melquiond2014-06-13