coq - The formal proof system

Age	Commit message (Expand)	Author
2015-01-18	Univs: proper printing of global and local universe names (only	Matthieu Sozeau
2015-01-12	Update headers.	Maxime Dénès
2014-12-16	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot
2014-11-20	Global.env chasing in Inv.	Pierre-Marie Pédrot
2014-10-22	Proofview: split [V82] module into [Unsafe] and [V82].	Arnaud Spiwack
2014-09-30	Seeing IntroWildcard as an action intro pattern rather than as a naming pattern	Hugo Herbelin
2014-09-11	Other bugs with "inversion as" (collision between user-provided names and gen...	Hugo Herbelin
2014-09-10	Fixing inversion after having fixed intros_replacing	Hugo Herbelin
2014-09-07	A better check that an "as" clause has been given to inversion, so	Hugo Herbelin
2014-09-07	Fixing "simple inversion as" (bug #2164).	Hugo Herbelin
2014-09-07	Dead code in inv.ml.	Hugo Herbelin
2014-09-06	Renaming goal-entering functions.	Pierre-Marie Pédrot
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