aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Expand)AuthorAge
...
* 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
* Deprecate options -dont, -lazy, -force-load-proofs.Gravatar Guillaume Melquiond2014-06-13
* Compute the trace of a universe inconsistency only when explicitly requiredGravatar Pierre-Marie Pédrot2014-06-10
* Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofGravatar Pierre-Marie Pédrot2014-06-08
* Timeout implementation for Windows based on threads.Gravatar Pierre-Marie Pédrot2014-06-08
* Enforce a correct exception handling in declaration_hooksGravatar Enrico Tassi2014-06-08
* Moving a Thread.yield in check_interrupt.Gravatar Pierre-Marie Pédrot2014-06-07
* Adding a new Control file centralizing the control options of Coq.Gravatar Pierre-Marie Pédrot2014-06-07
* Declare: fix Future managementGravatar Enrico Tassi2014-05-16
* Future: better error messageGravatar Enrico Tassi2014-05-15
* Moving Dnet-related code to tactics/.Gravatar Pierre-Marie Pédrot2014-05-08
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fixing ml-doc.Gravatar Pierre-Marie Pédrot2014-05-01
* Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toGravatar Hugo Herbelin2014-04-28
* Adding a stm/ folder, as asked during last workgroup. It was essentially movingGravatar Pierre-Marie Pédrot2014-04-25
* Future: memory optimization when forcing a chained pure computationGravatar Enrico Tassi2014-04-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-14 04:20:57 +0000