coq - The formal proof system

Age	Commit message (Expand)	Author
2014-01-30	Relaunch all Unix.waitpid when they ended with EINTR	Pierre Letouzey
2014-01-20	bug correction in proving principles of function	jforest
2014-01-10	Omega: avoiding distinct proof-terms on repeated identical runs	Pierre Letouzey
2013-12-24	Qed: feedback when type checking is done	Enrico Tassi
2013-12-20	micromega: removal of spurious Export; addition of Lia.v encapsulating lia an...	Frédéric Besson
2013-12-17	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot
2013-12-04	Fix g_derive.ml4.	Arnaud Spiwack
2013-12-04	Derive plugin.	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	Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.	Guillaume Melquiond
2013-12-03	Silence compilation warning by avoiding some deprecated constructs.	Guillaume Melquiond
2013-12-02	Writing [cut] tactic using the new monad.	Pierre-Marie Pédrot
2013-11-27	Getting rid of goal-dependency in declarative mode argument evaluation.	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-26	Do not use ugly Dyn features in the Quote plugin. Use instead the	Pierre-Marie Pédrot
2013-11-25	Remove the Hiddentac module.	Arnaud Spiwack
2013-11-21	Field_theory: nicer notations for constants 0 1 ...	Pierre Letouzey
2013-11-21	Add Acc_intro_generator on top of all wf function proof (much much faster exe...	Julien Forest
2013-11-15	bugfix micromega: solved an ambiguous symbol resolution	fbesson
2013-11-08	Porting Tactics.assumption to the new engine.	ppedrot
2013-11-02	Fix congruence: normalise hypotheses with respect to evars.	aspiwack
2013-11-02	Made Proofview.Goal.hyps a named_context.	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	Small syntax fix to be compatible with Ocaml 3.11.	aspiwack
2013-11-02	Adds a new goal selector "all:".	aspiwack
2013-11-02	Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).	aspiwack
2013-11-02	The tactic [admit] exits with the "unsafe" status.	aspiwack
2013-11-02	Cleanup of comments.	aspiwack
2013-11-02	Plug back the declarative mode.	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
2013-10-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-10-24	Rtree : cleanup of the comparing code	letouzey
2013-10-24	Oups, repair the compilation (micromega + Morphism_prop)	letouzey
2013-10-24	Get rid of polymorphic comparison in "plugins/btauto/refl_btauto.ml".	xclerc
2013-10-24	Turn many List.assoc into List.assoc_f	letouzey
2013-10-23	cList: a few alternative to hashtbl-based uniquize, distinct, subset	letouzey
2013-10-23	cList.index is now cList.index_f, same for index0	letouzey
2013-10-23	cList: set-as-list functions are now with an explicit comparison	letouzey
2013-10-18	declaration_hooks use Ephemeron	gareuselesinge
2013-10-16	Reintroduce "or" instead of "\|\|" as the latter is redifined in "sos_lib.ml" w...	xclerc
2013-10-14	Avoid polymorphic comparison (plugins/rtauto).	xclerc
2013-10-14	Avoid polymorphic comparison (plugins/cc).	xclerc
2013-10-14	Remove some uses of local modules (some were unused, some were costly).	xclerc