coq - The formal proof system

Age	Commit message (Expand)	Author
2014-01-05	Paral-ITP: cleanup of command line flags and more conservative default	Enrico Tassi
2014-01-05	Fix some warnings with ocamlc 4.01	Enrico Tassi
2014-01-05	coqtop: -check-vi-tasks and -schedule-vi-checking	Enrico Tassi
2014-01-04	Lemmas: export standard proof terminator	Enrico Tassi
2014-01-04	Proof_global: Simpler API for proof_terminator	Enrico Tassi
2014-01-04	STM: use sec vars in aux file if no Proof using when building .vi	Enrico Tassi
2014-01-04	.vi files: .vo files without proofs	Enrico Tassi
2014-01-04	STM: simple refactoring	Enrico Tassi
2014-01-04	STM: set loc for aux file when interpreting vernac	Enrico Tassi
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