coq - The formal proof system

Age	Commit message (Expand)	Author
2015-01-25	Adding a proper interface to Newring.	Pierre-Marie Pédrot
2015-01-21	Embedding the index of the ML tactic entry in the Tacexpr AST.	Pierre-Marie Pédrot
2015-01-12	Update headers.	Maxime Dénès
2014-10-31	Feedback message: hold extra info to help routing	Enrico Tassi
2014-10-27	Removing an Evd.merge in Newring.	Pierre-Marie Pédrot
2014-10-22	Proofview: split [V82] module into [Unsafe] and [V82].	Arnaud Spiwack
2014-09-12	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin
2014-09-06	Renaming goal-entering functions.	Pierre-Marie Pédrot
2014-08-18	Moving the TacExtend node from atomic to plain tactics.	Pierre-Marie Pédrot
2014-08-04	STM: VtQuery holds the id of the state it refers to	Carst Tankink
2014-07-27	Qualified ML tactic names. The plugin name is used to discriminate	Pierre-Marie Pédrot
2014-05-12	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot
2014-05-06	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau
2014-05-06	Rework handling of universes on top of the STM, allowing for delayed	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-28	Remove unused lookup table.	Guillaume Melquiond
2014-04-25	Removing useless try-with clauses in Goal.enter variants.	Pierre-Marie Pédrot
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2013-12-24	Qed: feedback when type checking is done	Enrico Tassi
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-10-05	Moving side effects into evar_map. There was no reason to keep another	ppedrot
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-08-30	add "Print Ring" and "Print Field" vernacular commands	gareuselesinge
2013-08-25	Added a more efficient way to recover the domain of a map.	ppedrot
2013-08-23	Fixing an incompleteness of the ring/field tactics	amahboub
2013-08-08	Vernac classification streamlined (handles VERNAC EXTEND)	gareuselesinge
2013-08-08	State Transaction Machine	gareuselesinge
2013-07-05	Expurgating the useless difference between List0 and List1 at the	ppedrot
2013-06-22	Now, idtac closures use maps instead of association list.	ppedrot
2013-06-21	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot
2013-06-10	Hiding tactic value representations.	ppedrot
2013-06-06	Uniformizing generic argument types.	ppedrot
2013-05-29	newring.ml4: interp constr arg at interp time (not parse time)	gareuselesinge
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-04-22	code simplifications concerning Summary	letouzey
2013-03-23	Minor code cleaning in CArray / CList.	ppedrot
2013-03-12	Allowing different types of, not to be mixed, generic Stores through	ppedrot
2013-02-19	Dir_path --> DirPath	letouzey
2013-02-18	Minor code cleanups, especially take advantage of Dir_path.is_empty	letouzey
2013-01-22	New implementation of the conversion test, using normalization by evaluation to	mdenes
2012-12-18	Modulification of Label	ppedrot
2012-12-14	Modulification of dir_path	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-12-14	Moved Stringset and Stringmap to String namespace.	ppedrot
2012-10-16	Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp	letouzey