aboutsummaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
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
2014-04-06Change handling of loadpath and mlpath.Guillaume Melquiond
2014-03-20Slightly more efficient Array.smartmap & related.Pierre-Marie Pédrot
2014-03-13Stateid: export a Set moduleEnrico Tassi
2014-03-13STM: move out a couple of submodulesEnrico Tassi
2014-03-12Stm: smarter delegation policyEnrico Tassi
2014-03-06Uses slashes for install and config directoriesVirgile Prevosto
2014-03-05Canary testing absence of generic equality for KerNamesPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 08:10:15 +0000