coq - The formal proof system

Age	Commit message (Expand)	Author
2014-08-05	Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].	Arnaud Spiwack
2014-08-04	Cleaning of the new implementation of the tactic monad.	Arnaud Spiwack
2014-08-01	Add primtive [num_goal] to Proofview.	Arnaud Spiwack
2014-08-01	Clean outdated comment in Proofview.Notations.	Arnaud Spiwack
2014-07-28	Adding a tclBREAK primitive to the tactic monad.	Pierre-Marie Pédrot
2014-07-25	Add a tactic [swap i j] to swap the position of goals [i] and [j].	Arnaud Spiwack
2014-07-25	Adds a cycle tactic to reorder goals in a loop.	Arnaud Spiwack
2014-07-24	A handful of useful primitives in Proofview.Refine.	Arnaud Spiwack
2014-07-23	Proof_global.start_dependent_proof: properly threads the sigma through the te...	Arnaud Spiwack
2014-07-13	Adding a "time" tactical for benchmarking purposes. In case the tactic	Hugo Herbelin
2014-07-10	check_for_interrupt: better (but slower) in threading mode	Enrico Tassi
2014-07-08	Exporting Proof.split in proofview.	Pierre-Marie Pédrot
2014-07-07	Revert "time tac" (committed by mistake).	Hugo Herbelin
2014-07-07	time tac	Hugo Herbelin
2014-06-19	Adding a raw_goals primitive for Tacinterp.	Pierre-Marie Pédrot
2014-06-18	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau
2014-06-03	The tactic interpreter now uses a new type of tactics, through	Pierre-Marie Pédrot
2014-05-24	Revert "Chasing the goal entering backward while interpreting tactics. This r...	Pierre-Marie Pédrot
2014-05-24	Chasing the goal entering backward while interpreting tactics. This required	Pierre-Marie Pédrot
2014-05-08	- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...	Matthieu Sozeau
2014-05-06	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-07	Transfering the initial goals from the proofview to the proof object.	Pierre-Marie Pédrot
2014-03-28	Lighter interface for creating refining tactics.	Pierre-Marie Pédrot
2014-03-26	Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.	Pierre-Marie Pédrot
2014-03-19	Adding phantom types to discriminate normalized goals, and adding a way to	Pierre-Marie Pédrot
2014-02-27	Code refactoring thanks to the new Monad module.	Arnaud Spiwack
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