coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	checker: less useless error messages	Enrico Tassi	2014-02-26
*	fix checker w.r.t. mutual_inductive_body and constant_body	Enrico Tassi	2014-02-26
*	fix checker w.r.t. Dyn.t validation	Enrico Tassi	2014-02-26
*	Future: make ~greedy:true the default + new sink commodity API	Enrico Tassi	2014-02-26
*	Future: each computation has a uuid	Enrico Tassi	2014-02-26
*	Tacinterp: remove the is_value check in Ltac's let-in.	Arnaud Spiwack	2014-02-25
*	Tacinterp: fewer enterl still.	Arnaud Spiwack	2014-02-25
*	Tacinterp: fewer Proofview.Goal.enterl.	Arnaud Spiwack	2014-02-25
*	Tacinterp: clean up.	Arnaud Spiwack	2014-02-25
*	Tacinterp: remove unnecessary return/bind pairs.	Arnaud Spiwack	2014-02-25
*	Fixing printing of only_parsing notations.	Pierre-Marie Pédrot	2014-02-25
*	TacticMatching: avoid some closure allocation in (<*>).	Arnaud Spiwack	2014-02-24
*	Removed some trailing whitespaces.	Arnaud Spiwack	2014-02-24
*	IStream: more efficient implementation of concat_map.	Arnaud Spiwack	2014-02-24
*	IStream: a concat_map primitive.	Arnaud Spiwack	2014-02-24
*	IStream: change type of thunk, spare allocations.	Arnaud Spiwack	2014-02-24
*	IStream: remove a useless Obj.magic.	Arnaud Spiwack	2014-02-24
*	A view type for IStream.	Arnaud Spiwack	2014-02-24
*	Ensuring that the module Stack is opaque inside Reductionops.	Pierre-Marie Pédrot	2014-02-24
*	make coqide-binaries does not build coqtop anymore	Pierre Boutillier	2014-02-24
*	fixup complement Fin	Pierre Boutillier	2014-02-24
*	cbn understands Arguments	Pierre Boutillier	2014-02-24
*	Simpl_behaviour becomes Reductionops.ReductionBehaviour	Pierre Boutillier	2014-02-24
*	Dead Code elimination	Pierre Boutillier	2014-02-24
*	Create Debug Unification option	Pierre Boutillier	2014-02-24
*	Fix coqide build under MacOS	Pierre Boutillier	2014-02-24
*	No more translation array <-> list in Reductionops.Stack	Pierre Boutillier	2014-02-24
*	Reductionops.Stack.strip* are ready to deal with Shift	Pierre Boutillier	2014-02-24
*	Reductionops.Stack.app_node is secret	Pierre Boutillier	2014-02-24
*	app_node, stack, state printers	Pierre Boutillier	2014-02-24
*	Stack operations of Reductionops in Reductionops.Stack	Pierre Boutillier	2014-02-24
*	Fix grammatical mistake in error message (bug #3238)	xclerc	2014-02-24
*	More sharing in Logic, together with some code cleaning.	Pierre-Marie Pédrot	2014-02-21
*	Optimization in kernel/vars.ml: directly allocate a fixed-size block in the	Pierre-Marie Pédrot	2014-02-20
*	CoqIDE: when coqtop misbehaves kill it properly (no zombie)	Enrico Tassi	2014-02-17
*	[nanoPG]: emacs like copy/paste	Enrico Tassi	2014-02-17
*	Removing non-marshallable data from the Agram constructor. Instead of	Pierre-Marie Pédrot	2014-02-16
*	fast correction of bug #3234	Julien Forest	2014-02-14
*	TC: honor the use_typeclasses flag in pretyping	Enrico Tassi	2014-02-12
*	Made Pre_env.lazy_val opaque.	Pierre-Marie Pédrot	2014-02-11
*	Timeout and Set Default Timeout fixed (closes: #3229)	Enrico Tassi	2014-02-10
*	STM: fix valid_id coming from Qed errors	Enrico Tassi	2014-02-10
*	STM: when a worker is canceled mark the proof as broken	Enrico Tassi	2014-02-10
*	STM: be conservative w.r.t. proofs containing global side effects	Enrico Tassi	2014-02-10
*	fake_ide: ported to spawn	Enrico Tassi	2014-02-10
*	Tentative fixup for the previous commit. It seems I have broken something	Pierre-Marie Pédrot	2014-02-10
*	Small optimizations in Closure:	Pierre-Marie Pédrot	2014-02-09
*	Less dependencies in Omega.	Pierre-Marie Pédrot	2014-02-08
*	FinFun.v: results about injective/surjective/bijective fonctions over finite ...	Pierre Letouzey	2014-02-07
*	Tactic extensions do not need to be classified by the STM, as	Pierre-Marie Pédrot	2014-02-05