aboutsummaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2014-10-13When loading libraries, feed back dependencies.Carst Tankink
2014-10-13STM: primitives to snapshot a .vi while in interactive modeEnrico Tassi
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-10-09Fixup leading ./ path cleaningPierre Boutillier
2014-10-07Splitting out of auto.ml a file hints.ml dedicated to hints so as toHugo Herbelin
2014-10-05A few improvements on pattern-matching compilation.Hugo Herbelin
2014-10-01STM: report the (structured) goals as XMLCarst Tankink
2014-09-25Remove some 'deprecated' warnings.Xavier Clerc
2014-09-18Fix debug printing with primitive projections.Matthieu Sozeau
2014-09-16Undo prints only if coqtop || emacsEnrico Tassi
2014-09-09Undo: if the ui is coqtop (command line) then Undo is not part of the doc.Enrico Tassi
2014-09-09toploop plugins taken into account when printing --help (close: 3535)Enrico Tassi
2014-09-08Removing dead code relative to the XML plugin.Pierre-Marie Pédrot
2014-09-05Adding a Ftactic module for potentially focussing tactics.Pierre-Marie Pédrot
2014-09-02coqworkmgrEnrico Tassi
2014-08-29Type-safe version of genarg list / pair / opt functions.Pierre-Marie Pédrot
2014-08-29Simplification of Genarg unpackers.Pierre-Marie Pédrot
2014-08-28Fixing bug #3541.Pierre-Marie Pédrot
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-08-05STM: new "par:" goal selector, like "all:" but in parallelEnrico Tassi
2014-08-05STM: code restructured to reuse task queue for tacticsEnrico Tassi
2014-08-04STM: encapsulate Pp.message in Feedback.feedbackCarst Tankink
2014-07-31Removing the call to Weak.get_copy in hashsets.Pierre-Marie Pédrot
2014-07-31Improve intersection of regular trees.Maxime Dénès
2014-07-29Pp: only one default feedback idEnrico Tassi
2014-07-29Pp compiles after feedbackEnrico Tassi
2014-07-24Revert "Adding a "is_val" primitive to IStream."Pierre-Marie Pédrot
2014-07-22Refine check_is_subterm.Maxime Dénès
2014-07-22Made intersection on regular trees less intensional.Maxime Dénès
2014-07-22Refining match subterm and commutative cut rules. The parameters that areMaxime Dénès
2014-07-22Adding a "is_val" primitive to IStream.Pierre-Marie Pédrot
2014-07-21Universe level maps use HMaps.Pierre-Marie Pédrot
2014-07-21Missing primitives in HMap.Pierre-Marie Pédrot
2014-07-21Fixing semantics of HSet.inter and HSet.diff.Pierre-Marie Pédrot
2014-07-13Adding a "time" tactical for benchmarking purposes. In case the tacticHugo Herbelin
2014-07-11An outdated comment + comment layout.Arnaud Spiwack
2014-07-11STM: let toploop plugins specify the flags for STM workersEnrico Tassi
2014-07-11STM: flag to turn off branch reopeningEnrico Tassi
2014-07-11Feedback: LoadedFile + GoalsEnrico Tassi
2014-07-11make the standard logging facility stm awareEnrico Tassi
2014-07-10option to always delegate futures to workersEnrico Tassi
2014-07-10more APIs in TQueue and CThreadEnrico Tassi
2014-07-10check_for_interrupt: better (but slower) in threading modeEnrico Tassi
2014-07-07Revert "time tac" (committed by mistake).Hugo Herbelin
2014-07-07time tacHugo Herbelin
2014-07-03Adding a coiterator to IStream.Pierre-Marie Pédrot
2014-06-25all coqide specific files moved into ide/Enrico Tassi
2014-06-21Less ocaml warnings.Hugo Herbelin
2014-06-13Deprecate useless option -quality.Guillaume Melquiond
2014-06-13Deprecate useless option -unsafe.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:36:19 +0000