coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	STM: fix for PG and "Proof term" lines.	gareuselesinge	2013-11-05
*	Fixup bug 3145	pboutill	2013-11-03
*	Adds a tactic give_up.	aspiwack	2013-11-02
*	Made multiple-goal tactic work after all: .	aspiwack	2013-11-02
*	Adds a shelve tactic.	aspiwack	2013-11-02
*	Less use of the list-based interface for goal-bound tactics.	aspiwack	2013-11-02
*	Tachmach.New is now in Proofview.Goal.enter style.	aspiwack	2013-11-02
*	More Proofview.Goal.enter.	aspiwack	2013-11-02
*	Fixes parsing of all: followed by a typechecking/evaluation command.	aspiwack	2013-11-02
*	Adds a new goal selector "all:".	aspiwack	2013-11-02
*	Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...	aspiwack	2013-11-02
*	Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).	aspiwack	2013-11-02
*	Clean up a warning.	aspiwack	2013-11-02
*	The tactic [admit] exits with the "unsafe" status.	aspiwack	2013-11-02
*	Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.	aspiwack	2013-11-02
*	Getting rid of Goal.here, and all the related exceptions and combinators.	aspiwack	2013-11-02
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	Future: better doc + restore ~pure optimization	gareuselesinge	2013-10-31
*	Conv_orable made functional and part of pre_env	gareuselesinge	2013-10-31
*	Revert the two last commits. My bad, I messed up git-svn commands...	ppedrot	2013-10-29
*	Profile only when CAMLRUNPARAM is set.	ppedrot	2013-10-29
*	Printing heap on every processed sentence.	ppedrot	2013-10-29
*	Removing Evd.undefined_evars.	ppedrot	2013-10-28
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
*	cList: a few alternative to hashtbl-based uniquize, distinct, subset	letouzey	2013-10-23
*	cList.index is now cList.index_f, same for index0	letouzey	2013-10-23
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23
*	Moving potentially costly computation from exception raising to message	ppedrot	2013-10-22
*	STM: proper error message if the GUI edits_at a dummy state	gareuselesinge	2013-10-22
*	STM: do not enrich exceptions more than once	gareuselesinge	2013-10-22
*	STM: send the gui the status of the slaves	gareuselesinge	2013-10-22
*	Coqtop: fix looping over a broken state.	gareuselesinge	2013-10-18
*	declaration_hooks use Ephemeron	gareuselesinge	2013-10-18
*	Future: ported to Ephemeron + exception enhancing	gareuselesinge	2013-10-18
*	STM: not optimize proofs containing an Undo	gareuselesinge	2013-10-18
*	Remove some uses of local modules (some were unused, some were costly).	xclerc	2013-10-14
*	STM: prefix debug messages with slave-id	gareuselesinge	2013-10-11
*	More comments in ide_slave	gareuselesinge	2013-10-11
*	STM: cancel slaves working on outdated jobs	gareuselesinge	2013-10-11
*	STM: a proof with nested proofs cannot be delegated	gareuselesinge	2013-10-10
*	STM: add "Stm Wait" to wait for the slaves to complete their jobs	gareuselesinge	2013-10-10
*	Clib: fold_left_until added to CList	gareuselesinge	2013-10-10
*	STM: new command "Stm PrintDag" to force printing the dag to /tmp	gareuselesinge	2013-10-07
*	STM: fix verbosity of queries	gareuselesinge	2013-10-07
*	STM: spit a warning if an out of bound Back* command is issued	gareuselesinge	2013-10-07
*	coqtop: init STM before loading rcfile	gareuselesinge	2013-10-07
*	Removing uses of Evar.add in class-related functions.	ppedrot	2013-10-06
*	Removing dubious use of evarmap manipulating functions in printing	ppedrot	2013-10-05
*	Moving side effects into evar_map. There was no reason to keep another	ppedrot	2013-10-05