coq - The formal proof system

Age	Commit message (Expand)	Author
2013-11-04	Allowing proofs starting with a non-empty evarmap.	ppedrot
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	Fix destruct: nf_evar prior to tactic interpretation.	aspiwack
2013-11-02	Add primitives in Goal.V82 to access the goal in nf_evar'd form.	aspiwack
2013-11-02	Adds a tactic give_up.	aspiwack
2013-11-02	A tactic shelve_unifiable.	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	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	A dedicated view type for Proofview_gen.split.	aspiwack
2013-11-02	Adds a tactical once.	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	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	Makes the Ltac debugger usable again.	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	The tactic [admit] exits with the "unsafe" status.	aspiwack
2013-11-02	Cleanup of comments.	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	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-10-31	Future: better doc + restore ~pure optimization	gareuselesinge
2013-10-31	Conv_orable made functional and part of pre_env	gareuselesinge
2013-10-29	Do not generate useless argument arrays in whd_* functions.	ppedrot
2013-10-28	Useless array to list conversions in proof/logic.ml.	ppedrot
2013-10-27	Abstracting evar filter away. The API is not perfect, but better than nothing.	ppedrot
2013-10-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-10-23	cList: a few alternative to hashtbl-based uniquize, distinct, subset	letouzey