coq - The formal proof system

Age	Commit message (Expand)	Author
2013-12-24	Qed: feedback when type checking is done	Enrico Tassi
2013-12-17	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot
2013-12-11	Fixing backtrace registering of various tactic-related try-with blocks.	Pierre-Marie Pédrot
2013-12-04	Fix Admitted.	Arnaud Spiwack
2013-12-04	Proof_global: fix start_proof comment after the preceding commits.	Arnaud Spiwack
2013-12-04	Factoring(continued).	Arnaud Spiwack
2013-12-04	Refactoring: storing more information in the terminator closure.	Arnaud Spiwack
2013-12-04	The commands that initiate proofs are now in charge of what happens when proo...	Arnaud Spiwack
2013-12-04	Allow proofs to start with dependent goals.	Arnaud Spiwack
2013-11-30	Fixing ltac constr variable handling in refine.	Pierre-Marie Pédrot
2013-11-29	Fixing bug #3169 and avoiding anomaly in bug #2885 (vm_compute not	Hugo Herbelin
2013-11-12	Useless computation in Goal handle augmentation.	ppedrot
2013-11-12	Do not print tactic notation names at each interpretation step.	ppedrot
2013-11-09	Partial applications in Goal.	ppedrot
2013-11-07	Rewriting the proof monad mechanism. Now it uses pure OCaml code, without	ppedrot
2013-11-06	Less partial applications in Vars, as well as better memory allocation.	ppedrot
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	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