coq - The formal proof system

Age	Commit message (Expand)	Author
2014-01-30	Fixing backtrace handling here and there.	Pierre-Marie Pédrot
2013-12-11	Fixing backtrace registering of various tactic-related try-with blocks.	Pierre-Marie Pédrot
2013-12-04	Allow proofs to start with dependent goals.	Arnaud Spiwack
2013-11-05	Reducing allocation in tclDISPATCHGEN, by doing a List.map at the same time	ppedrot
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	A try/with was catching every exception.	aspiwack
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	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	Adds an experimental exactly_once tactical.	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	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	Uses Proofview.tclEXTEND more sparingly.	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-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-09-03	Partly replacing list-based access functions in Evd. This is still	ppedrot
2013-08-08	State Transaction Machine	gareuselesinge
2013-06-06	Fixing bug #3030.	ppedrot
2013-05-28	Getting rid of LtacLocated exception transformer.	ppedrot
2013-02-18	Removing Exc_located and using the new exception enrichement	ppedrot
2013-02-17	Added propagation of evars unification failure reasons for better	herbelin
2013-02-17	Revised the Ltac trace mechanism so that trace breaking due to	herbelin
2012-12-14	Moved Intset and Intmap to Int namespace.	ppedrot
2012-11-25	Monomorphization (proof)	ppedrot
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-14	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot
2012-09-14	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia
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