aboutsummaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
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
2014-06-13Deprecate options -dont, -lazy, -force-load-proofs.Guillaume Melquiond
2014-06-10Compute the trace of a universe inconsistency only when explicitly requiredPierre-Marie Pédrot
2014-06-08Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofPierre-Marie Pédrot
2014-06-08Timeout implementation for Windows based on threads.Pierre-Marie Pédrot
2014-06-08Enforce a correct exception handling in declaration_hooksEnrico Tassi
2014-06-07Moving a Thread.yield in check_interrupt.Pierre-Marie Pédrot
2014-06-07Adding a new Control file centralizing the control options of Coq.Pierre-Marie Pédrot
2014-05-16Declare: fix Future managementEnrico Tassi
2014-05-15Future: better error messageEnrico Tassi
2014-05-08Moving Dnet-related code to tactics/.Pierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-05-01Fixing ml-doc.Pierre-Marie Pédrot
2014-04-28Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toHugo Herbelin
2014-04-25Adding a stm/ folder, as asked during last workgroup. It was essentially movingPierre-Marie Pédrot
2014-04-25Future: memory optimization when forcing a chained pure computationEnrico Tassi
2014-04-25Adding a debug printer for futures.Pierre-Marie Pédrot
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-04-10Have the feedback bus as a backend for dumping globs.Carst Tankink
2014-04-09Removing handshake from Spawn. It used marshalling, which is bad forPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:20:14 +0000