coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	coqtop: -check-vi-tasks and -schedule-vi-checking	Enrico Tassi	2014-01-05
*	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	2014-01-04
*	Useless Evd.create_evar_defs.	Pierre-Marie Pédrot	2013-12-30
*	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-24
*	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-22
*	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot	2013-12-17
*	A few fixes to the build system (mostly for ocamlbuild)	Pierre Letouzey	2013-12-16
*	Fix CoqIDE on windows	Enrico Tassi	2013-12-10
*	Fix printing of Ltac's backtrace.	Arnaud Spiwack	2013-12-09
*	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-04
*	Removing useless meta-related functions.	Pierre-Marie Pédrot	2013-12-03
*	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-27
*	Remove the Hiddentac module.	Arnaud Spiwack	2013-11-25
*	Using hashes instead of strings in dynamic tags. In case of collision, an	Pierre-Marie Pédrot	2013-11-22
*	Do not print tactic notation names at each interpretation step.	ppedrot	2013-11-12
*	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-10
*	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-09
*	STM: fix for PG and "Proof term" lines.	gareuselesinge	2013-11-05
*	Fixup bug 3145	pboutill	2013-11-03
*	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