coq - The formal proof system

Age	Commit message (Expand)	Author
2014-02-27	Remove unsafe code (Obj.magic) in Tacinterp.	Arnaud Spiwack
2014-02-27	Proofview.Notations: Now that (>>=) is free, use it for tclBIND.	Arnaud Spiwack
2014-02-27	Get rid of the enterl/glist API for Proofview.Goal.	Arnaud Spiwack
2014-02-25	Tacinterp: fewer Proofview.Goal.enterl.	Arnaud Spiwack
2014-01-31	Typos in comment.	Arnaud Spiwack
2013-12-04	Allow proofs to start with dependent goals.	Arnaud Spiwack
2013-11-04	Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was sol...	aspiwack
2013-11-04	Fix the tactical ; [ … ] : the "incorrect number of goal" error was not cau...	aspiwack
2013-11-04	Allowing proofs starting with a non-empty evarmap.	ppedrot
2013-11-02	Update comments.	aspiwack
2013-11-02	Fix destruct: nf_evar prior to tactic interpretation.	aspiwack
2013-11-02	Adds a tactic give_up.	aspiwack
2013-11-02	A tactic shelve_unifiable.	aspiwack
2013-11-02	Adds a shelve tactic.	aspiwack
2013-11-02	Adds an experimental exactly_once tactical.	aspiwack
2013-11-02	Made Proofview.Goal.hyps a named_context.	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	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	Makes the Ltac debugger usable again.	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	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	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack
2013-10-05	Moving side effects into evar_map. There was no reason to keep another	ppedrot
2013-08-08	State Transaction Machine	gareuselesinge
2012-08-08	Updating headers.	herbelin
2012-07-11	Severe reorganisation of the code of tactics in Proofview.	aspiwack
2012-07-10	Small change in the printing of proofs for use by coqide.	aspiwack
2012-07-04	Change how the number of open goals is printed.	aspiwack
2012-05-29	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey
2012-02-07	A "Grab Existential Variables" to transform the unresolved evars at the end o...	aspiwack
2011-11-23	In emacs mode, prints a list of the dependent existential variables introduced	aspiwack
2011-09-12	Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...	aspiwack
2011-08-10	Fixing typos in comments	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-22	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack