coq - The formal proof system

Age	Commit message (Expand)	Author
2013-11-02	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	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