coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
*	Univs: proper printing of global and local universe names (only	Matthieu Sozeau	2015-01-17
*	Update headers.	Maxime Dénès	2015-01-12
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Global.env chasing in Inv.	Pierre-Marie Pédrot	2014-11-20
*	Proofview: split [V82] module into [Unsafe] and [V82].	Arnaud Spiwack	2014-10-22
*	Seeing IntroWildcard as an action intro pattern rather than as a naming pattern	Hugo Herbelin	2014-09-30
*	Other bugs with "inversion as" (collision between user-provided names and gen...	Hugo Herbelin	2014-09-11
*	Fixing inversion after having fixed intros_replacing	Hugo Herbelin	2014-09-10
*	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-07
*	Renaming goal-entering functions.	Pierre-Marie Pédrot	2014-09-06
*	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-18
*	In Hipattern: some functions not working modulo evar instantiation.	Arnaud Spiwack	2014-08-07
*	Experimentally adding an option for automatically erasing an	Hugo Herbelin	2014-08-05
*	Fix program cases and inversion tactic to correctly record universe constraints.	Matthieu Sozeau	2014-06-24
*	Add an e_type_of to avoid losing universe constraints.	Matthieu Sozeau	2014-06-20
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Giving true proof-terms in inversion instead of metas.	Pierre-Marie Pédrot	2014-04-27
*	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot	2014-04-23
*	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-04-22
*	Define Tactics.bring_hyps in the new monad.	Pierre-Marie Pédrot	2014-03-28
*	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-03-26
*	Proofview.Notations: Now that (>>=) is free, use it for tclBIND.	Arnaud Spiwack	2014-02-27
*	Fixing dependent inversion. Some exceptions were not caught by the tactic	Pierre-Marie Pédrot	2014-01-28
*	Remove some occurrences of obsolete operators	Stephane Glondu	2013-11-22
*	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-11-02
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	Revising r16550 about providing intro patterns for applying injection:	herbelin	2013-07-09
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Minor code cleaning in CArray / CList.	ppedrot	2013-03-23
*	Restrict (try...with...) to avoid catching critical exn (part 10)	letouzey	2013-03-13
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (tactics)	ppedrot	2012-11-25
*	Improving error message when abtraction over goal (abstract_list_all	herbelin	2012-10-04
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14