aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-02-25Fixing printing of only_parsing notations.Pierre-Marie Pédrot
2014-02-24TacticMatching: avoid some closure allocation in (<*>).Arnaud Spiwack
2014-02-24Removed some trailing whitespaces.Arnaud Spiwack
2014-02-24IStream: more efficient implementation of concat_map.Arnaud Spiwack
2014-02-24IStream: a concat_map primitive.Arnaud Spiwack
2014-02-24IStream: change type of thunk, spare allocations.Arnaud Spiwack
2014-02-24IStream: remove a useless Obj.magic.Arnaud Spiwack
2014-02-24A view type for IStream.Arnaud Spiwack
2014-02-24Ensuring that the module Stack is opaque inside Reductionops.Pierre-Marie Pédrot
2014-02-24make coqide-binaries does not build coqtop anymorePierre Boutillier
2014-02-24fixup complement FinPierre Boutillier
2014-02-24cbn understands ArgumentsPierre Boutillier
2014-02-24Simpl_behaviour becomes Reductionops.ReductionBehaviourPierre Boutillier
2014-02-24Dead Code eliminationPierre Boutillier
2014-02-24Create Debug Unification optionPierre Boutillier
2014-02-24Fix coqide build under MacOSPierre Boutillier
2014-02-24No more translation array <-> list in Reductionops.StackPierre Boutillier
2014-02-24Reductionops.Stack.strip* are ready to deal with ShiftPierre Boutillier
2014-02-24Reductionops.Stack.app_node is secretPierre Boutillier
2014-02-24app_node, stack, state printersPierre Boutillier
2014-02-24Stack operations of Reductionops in Reductionops.StackPierre Boutillier
2014-02-24Fix grammatical mistake in error message (bug #3238)xclerc
2014-02-21More sharing in Logic, together with some code cleaning.Pierre-Marie Pédrot
2014-02-20Optimization in kernel/vars.ml: directly allocate a fixed-size block in thePierre-Marie Pédrot
2014-02-17CoqIDE: when coqtop misbehaves kill it properly (no zombie)Enrico Tassi
2014-02-17[nanoPG]: emacs like copy/pasteEnrico Tassi
2014-02-16Removing non-marshallable data from the Agram constructor. Instead ofPierre-Marie Pédrot
2014-02-14fast correction of bug #3234Julien Forest
2014-02-12TC: honor the use_typeclasses flag in pretypingEnrico Tassi
2014-02-11Made Pre_env.lazy_val opaque.Pierre-Marie Pédrot
2014-02-10Timeout and Set Default Timeout fixed (closes: #3229)Enrico Tassi
2014-02-10STM: fix valid_id coming from Qed errorsEnrico Tassi
2014-02-10STM: when a worker is canceled mark the proof as brokenEnrico Tassi
2014-02-10STM: be conservative w.r.t. proofs containing global side effectsEnrico Tassi
2014-02-10fake_ide: ported to spawnEnrico Tassi
2014-02-10Tentative fixup for the previous commit. It seems I have broken somethingPierre-Marie Pédrot
2014-02-09Small optimizations in Closure:Pierre-Marie Pédrot
2014-02-08Less dependencies in Omega.Pierre-Marie Pédrot
2014-02-07FinFun.v: results about injective/surjective/bijective fonctions over finite ...Pierre Letouzey
2014-02-05Tactic extensions do not need to be classified by the STM, asPierre-Marie Pédrot
2014-02-04The constructor tactic now returns several successes.Pierre-Marie Pédrot
2014-02-03Tracking memory misallocation by trying to improve sharing.Pierre-Marie Pédrot
2014-02-03Allocation-friendly mapping functions in Nametab.Pierre-Marie Pédrot
2014-02-03Allocation friendly map-handling functions in Dag.Pierre-Marie Pédrot
2014-02-02Fixing backtrace reporting.Pierre-Marie Pédrot
2014-02-02Fixing bug #3226.Pierre-Marie Pédrot
2014-02-02Removing the [Require "file"] syntax.Pierre-Marie Pédrot
2014-01-31In Ltac's exact tactic: avoid checking the type of the term twice.Arnaud Spiwack
2014-01-31Typos in comment.Arnaud Spiwack
2014-01-30Coqmktop without Sys.command, changes in ./configure -*byteflags optionsPierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 10:18:43 +0000