coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	More Proofview.Goal.enter.	aspiwack	2013-11-02
*	A better version of Goal.advance.	aspiwack	2013-11-02
*	Added the tactical "tac1 + tac2".	aspiwack	2013-11-02
*	Typos in a comment.	aspiwack	2013-11-02
*	bootstrap/Monads.v: A more efficient split.	aspiwack	2013-11-02
*	State monad implemented in CPS.	aspiwack	2013-11-02
*	A more principled split.	aspiwack	2013-11-02
*	Set an extraction flag for inling let-s in Monad.v.	aspiwack	2013-11-02
*	More optimisations of partial applications.	aspiwack	2013-11-02
*	Try to remove intermediate allocations when dealing with goal-specific tactics.	aspiwack	2013-11-02
*	Various rewriting, mostly for speed purposes.	aspiwack	2013-11-02
*	Optimisation of partial applications in the tactic monad.	aspiwack	2013-11-02
*	Fixes parsing of all: followed by a typechecking/evaluation command.	aspiwack	2013-11-02
*	Fix behaviour of the refine tactic with respect to evars in types.	aspiwack	2013-11-02
*	Small syntax fix to be compatible with Ocaml 3.11.	aspiwack	2013-11-02
*	Makes the Ltac debugger usable again.	aspiwack	2013-11-02
*	Document "all:" and "Set Default Goal Selector".	aspiwack	2013-11-02
*	New option Default Goal Selector.	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
*	Removes Refine from the dev tools now that the module has been deleted.	aspiwack	2013-11-02
*	Clean up a warning.	aspiwack	2013-11-02
*	The tactic [admit] exits with the "unsafe" status.	aspiwack	2013-11-02
*	Cleanup of comments.	aspiwack	2013-11-02
*	Plug back the declarative mode.	aspiwack	2013-11-02
*	Small change to the IO monad interface: [val ref : 'a -> 'a ref t]	aspiwack	2013-11-02
*	A whole new implemenation of the refine tactic.	aspiwack	2013-11-02
*	A newly introduced variable inside a named context is no longer α-renamed.	aspiwack	2013-11-02
*	Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.	aspiwack	2013-11-02
*	Bases tactics on an IO monad.	aspiwack	2013-11-02
*	Getting rid of Goal.here, and all the related exceptions and combinators.	aspiwack	2013-11-02
*	Uses Proofview.tclEXTEND more sparingly.	aspiwack	2013-11-02
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	Closure: fix an issue with r16959 spotted by Matthieu	letouzey	2013-11-02
*	Mod_subst.update_delta_resolver : avoid loosing Inline(_,Some _)	letouzey	2013-10-31
*	Fixing Kerpair.hash. Since the beginning, it dit not respect the type	ppedrot	2013-10-31
*	Future: better doc + restore ~pure optimization	gareuselesinge	2013-10-31
*	CoqIDE: scroll to the right position if there is an interp error	gareuselesinge	2013-10-31
*	Conv_orable made functional and part of pre_env	gareuselesinge	2013-10-31
*	Efficient filtered functions in Evd. We test that a filter is actually	ppedrot	2013-10-31
*	Avoiding useless allocations in Closure.	ppedrot	2013-10-31
*	Various optimizations of Evd.meta_* functions.	ppedrot	2013-10-30
*	More efficient implementation of [Evd.retract_coercible_metas].	ppedrot	2013-10-30
*	Optimization in unification: when checking that the head of a term is an	ppedrot	2013-10-29
*	Useless array-to-list casts in Unification.	ppedrot	2013-10-29
*	Do not generate useless argument arrays in whd_* functions.	ppedrot	2013-10-29
*	Prevent [Evarutil.whd_head_evar] from uselessly reallocating arrays.	ppedrot	2013-10-29
*	[Reductionops.append_stack_app]: do not allocate a useless array.	ppedrot	2013-10-29
*	Revert the two last commits. My bad, I messed up git-svn commands...	ppedrot	2013-10-29