coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Tacinterp: more refactoring.	Arnaud Spiwack	2014-02-27
*	Tacinterp: refactoring using Monad.	Arnaud Spiwack	2014-02-27
*	Code refactoring thanks to the new Monad module.	Arnaud Spiwack	2014-02-27
*	Remove unsafe code (Obj.magic) in Tacinterp.	Arnaud Spiwack	2014-02-27
*	Proofview.Notations: Now that (>>=) is free, use it for tclBIND.	Arnaud Spiwack	2014-02-27
*	Get rid of the enterl/glist API for Proofview.Goal.	Arnaud Spiwack	2014-02-27
*	Tacinterp: yet another superfluous enterl.	Arnaud Spiwack	2014-02-27
*	Tacinterp: spurious enterl.	Arnaud Spiwack	2014-02-27
*	Dead code: eval_ltac_constr.	Arnaud Spiwack	2014-02-27
*	STM: better debug messages	Enrico Tassi	2014-02-26
*	STM: do not print goals on Undo	Enrico Tassi	2014-02-26
*	CoqIDE: print message of "Fail" command	Enrico Tassi	2014-02-26
*	refman: document vi2vo	Enrico Tassi	2014-02-26
*	STM: better messages when checking/finishing tasks	Enrico Tassi	2014-02-26
*	Library: when compiling multiple files, reset the opaque tables	Enrico Tassi	2014-02-26
*	STM: when batch compiling a vo, assert we behave conservatively	Enrico Tassi	2014-02-26
*	coq_makefile: new target vi2vo	Enrico Tassi	2014-02-26
*	vi2vo: new flag -schedule-vi2vo	Enrico Tassi	2014-02-26
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26
*	STM: backup/restore remote counters	Enrico Tassi	2014-02-26
*	remoteCounter: backup/restore	Enrico Tassi	2014-02-26
*	univ: removing dead code	Enrico Tassi	2014-02-26
*	checker and votour ported to new vo format (after -vi2vo)	Enrico Tassi	2014-02-26
*	New compilation mode -vi2vo	Enrico Tassi	2014-02-26
*	votour: better error messages	Enrico Tassi	2014-02-26
*	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