coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	empty token in terminal is a user error not an anomaly (bug 3118)	pboutill	2013-11-03
*	test-suite fixup	pboutill	2013-11-03
*	Asks camlp5 binary in path its location	pboutill	2013-11-03
*	Fixup bug 3145	pboutill	2013-11-03
*	configure stript allows make v4.00	pboutill	2013-11-03
*	Fixing CAMLP4 compilation.	ppedrot	2013-11-02
*	Fix set: nf_evar prior to tactic interpretation.	aspiwack	2013-11-02
*	Plug back infoH.	aspiwack	2013-11-02
*	Plugs back external tactics.	aspiwack	2013-11-02
*	Fix the log of debug auto.	aspiwack	2013-11-02
*	A try/with was catching every exception.	aspiwack	2013-11-02
*	Update comments.	aspiwack	2013-11-02
*	Doc: solve the bad interaction between Declare Implicit Tactic and refine.	aspiwack	2013-11-02
*	Cleanup of comments in bootstrap/Monads.v	aspiwack	2013-11-02
*	The repeat tactic now honors failure levels in ltac.	aspiwack	2013-11-02
*	Documentation for the backtracking features.	aspiwack	2013-11-02
*	Fix destruct: nf_evar prior to tactic interpretation.	aspiwack	2013-11-02
*	Tacticals.New.tclWITHHOLES: clean up.	aspiwack	2013-11-02
*	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