coq - The formal proof system

Age	Commit message (Expand)	Author
2014-01-04	STM: record in aux file proof build and check time	Enrico Tassi
2013-12-30	Useless Evd.create_evar_defs.	Pierre-Marie Pédrot
2013-12-24	STM: capture type checking error (Closes: 3195)	Enrico Tassi
2013-12-24	Qed: feedback when type checking is done	Enrico Tassi
2013-12-24	CoqIDE: new feedback "incomplete" to signal partial Qed	Enrico Tassi
2013-12-24	cleanup warning	Enrico Tassi
2013-12-22	Adding a finer-grained -bt flag to coqtop only triggering backtraces.	Pierre-Marie Pédrot
2013-12-22	Notations can now accept dummy arguments. If ever a bound variable is not	Pierre-Marie Pédrot
2013-12-17	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot
2013-12-16	A few fixes to the build system (mostly for ocamlbuild)	Pierre Letouzey
2013-12-10	Fix CoqIDE on windows	Enrico Tassi
2013-12-09	Fix printing of Ltac's backtrace.	Arnaud Spiwack
2013-12-04	Stm: remove an assertion.	Arnaud Spiwack
2013-12-04	Fix Admitted.	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	Vernac classification: allow for commands which start proofs but must be sync...	Arnaud Spiwack
2013-12-03	Removing useless meta-related functions.	Pierre-Marie Pédrot
2013-11-27	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot
2013-11-27	Old message Interp returns the state id so that one can BackTo it	Enrico Tassi
2013-11-27	New option --help-XML-protocol to document the XML procol used by -ideslave	Enrico Tassi
2013-11-27	First stab at retrocompatible INTERP message	Enrico Tassi
2013-11-27	STM: restart slave after every proof	Enrico Tassi
2013-11-25	Remove the Hiddentac module.	Arnaud Spiwack
2013-11-22	Using hashes instead of strings in dynamic tags. In case of collision, an	Pierre-Marie Pédrot
2013-11-12	Do not print tactic notation names at each interpretation step.	ppedrot
2013-11-10	Centralizing the Ltac-defining functions in Tacenv.	ppedrot
2013-11-10	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot
2013-11-09	Revert the previous commit. It broke Coq compilation.	ppedrot
2013-11-09	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot
2013-11-09	Moving notation types into grammar rule.	ppedrot
2013-11-09	Cleaning and documenting Egramcoq.	ppedrot
2013-11-05	STM: fix for PG and "Proof term" lines.	gareuselesinge
2013-11-03	Fixup bug 3145	pboutill
2013-11-02	Adds a tactic give_up.	aspiwack
2013-11-02	Made multiple-goal tactic work after all: .	aspiwack
2013-11-02	Adds a shelve tactic.	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	Fixes parsing of all: followed by a typechecking/evaluation command.	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	Clean up a warning.	aspiwack
2013-11-02	The tactic [admit] exits with the "unsafe" status.	aspiwack
2013-11-02	Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.	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