coq - The formal proof system

Age	Commit message (Expand)	Author
2014-08-18	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin
2014-08-18	A reorganization of the "assert" tactics (hopefully uniform naming	Hugo Herbelin
2014-08-18	Reorganisation of intropattern code	Hugo Herbelin
2014-08-07	In Hipattern: some functions not working modulo evar instantiation.	Arnaud Spiwack
2014-08-05	Experimentally adding an option for automatically erasing an	Hugo Herbelin
2014-06-24	Fix program cases and inversion tactic to correctly record universe constraints.	Matthieu Sozeau
2014-06-20	Add an e_type_of to avoid losing universe constraints.	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-27	Giving true proof-terms in inversion instead of metas.	Pierre-Marie Pédrot
2014-04-23	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot
2014-04-22	Using the new monad tactic in Inv.	Pierre-Marie Pédrot
2014-04-22	Removing tactic compatibility layer from Elim.	Pierre-Marie Pédrot
2014-04-22	Simplifying interface of elimination tactics. They used dummy clausenvs, and	Pierre-Marie Pédrot
2014-03-28	Define Tactics.bring_hyps in the new monad.	Pierre-Marie Pédrot
2014-03-26	Removing Tacmach compatibility layer in Inv.	Pierre-Marie Pédrot
2014-03-26	Removing tactic compatibility layer from Inv.	Pierre-Marie Pédrot
2014-03-26	Moving some tactic code to the new engine.	Pierre-Marie Pédrot
2014-02-27	Proofview.Notations: Now that (>>=) is free, use it for tclBIND.	Arnaud Spiwack
2014-01-28	Fixing dependent inversion. Some exceptions were not caught by the tactic	Pierre-Marie Pédrot
2013-11-22	Remove some occurrences of obsolete operators	Stephane Glondu
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	Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).	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-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-07-09	Revising r16550 about providing intro patterns for applying injection:	herbelin
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-03-23	Minor code cleaning in CArray / CList.	ppedrot
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 10)	letouzey
2012-12-14	Modulification of identifier	ppedrot
2012-11-25	Monomorphization (tactics)	ppedrot
2012-10-04	Improving error message when abtraction over goal (abstract_list_all	herbelin
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-14	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot
2012-09-14	This patch removes unused "open" (automatically generated from	regisgia
2012-09-14	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia
2012-08-08	Updating headers.	herbelin
2012-05-29	Tacexpr as a mli-only, the few functions there are now in Tacops	letouzey
2012-05-29	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey
2012-03-02	Noise for nothing	pboutill
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-13	Made intros_until and onInductionArg a bit stricter and robust	herbelin
2010-06-12	Fixed bug #2135 (second-order unification was raising cryptic message)	herbelin
2010-06-12	Fixing spelling: pr_coma -> pr_comma	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin