coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix congruence: normalise hypotheses with respect to evars.	aspiwack	2013-11-02
*	Add primitives in Goal.V82 to access the goal in nf_evar'd form.	aspiwack	2013-11-02
*	push_rel_context: do not rename section variables.	aspiwack	2013-11-02
*	Refine now does iota reduction in addition to beta.	aspiwack	2013-11-02
*	Fix compilation of pattern matching wrt variables: alias.	aspiwack	2013-11-02
*	Restore Zsqrt compat now that refine works fine with match.	aspiwack	2013-11-02
*	Fix the compilation of pattern matching wrt to variables.	aspiwack	2013-11-02
*	Refine: Tactics.New.refine does beta-reduction.	aspiwack	2013-11-02
*	Adds a tactic give_up.	aspiwack	2013-11-02
*	A tactic shelve_unifiable.	aspiwack	2013-11-02
*	Made multiple-goal tactic work after all: .	aspiwack	2013-11-02
*	Make multiple-goal tactics possible after a tclTHEN.	aspiwack	2013-11-02
*	Corrects a bug on Proofview.Goal.enter whereby sigmas were captured and used ...	aspiwack	2013-11-02
*	Adds a shelve tactic.	aspiwack	2013-11-02
*	bootstrap/Monad.v: implements the writer monad in continuation passing style.	aspiwack	2013-11-02
*	bootstrap/Monad.v: implements the environment monad in continuation passing s...	aspiwack	2013-11-02
*	Factors the lifting of environment and writer monads in bootstrap/Monad.v	aspiwack	2013-11-02
*	Adds an experimental exactly_once tactical.	aspiwack	2013-11-02
*	Normalise goals with respect to evars in the new tactics.	aspiwack	2013-11-02
*	Made Proofview.Goal.hyps a named_context.	aspiwack	2013-11-02
*	Refine does beta-reductions.	aspiwack	2013-11-02
*	A dedicated view type for Proofview_gen.split.	aspiwack	2013-11-02
*	Adds a tactical once.	aspiwack	2013-11-02
*	Corrects the semantics of the "+" tactical.	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
*	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