coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Using dynamic values in tactic evaluation.	Pierre-Marie Pédrot	2015-12-21
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\
\| *	Fix some typos.	Guillaume Melquiond	2015-12-07
* \|	Getting rid of dynamic hacks in Setoid_newring.	Pierre-Marie Pédrot	2015-12-04
* \|	Removing the last use of tacticIn in setoid_ring.	Pierre-Marie Pédrot	2015-12-03
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\\|
\| *	Univs: local names handling.	Matthieu Sozeau	2015-10-28
* \|	Proofview.Goal.sigma returns an indexed evarmap.	Pierre-Marie Pédrot	2015-10-20
* \|	Boxing the Goal.enter primitive into a record type.	Pierre-Marie Pédrot	2015-10-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\|
\| *	Univs: fix evar_map initialization in newring.	Matthieu Sozeau	2015-10-02
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
\| *	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
\| *	Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)	Hugo Herbelin	2015-02-12
\| *	Capital letter in plugins.	Hugo Herbelin	2015-02-12
* \|	Adding a proper interface to Newring.	Pierre-Marie Pédrot	2015-01-25
* \|	Embedding the index of the ML tactic entry in the Tacexpr AST.	Pierre-Marie Pédrot	2015-01-21
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Feedback message: hold extra info to help routing	Enrico Tassi	2014-10-31
*	Removing an Evd.merge in Newring.	Pierre-Marie Pédrot	2014-10-27
*	Fix some typos in comments.	Guillaume Melquiond	2014-10-27
*	Proofview: split [V82] module into [Unsafe] and [V82].	Arnaud Spiwack	2014-10-22
*	Fix cbn behavior wrt simpl no match	Pierre Boutillier	2014-10-01
*	Keyed unification option, compiling the whole standard library	Matthieu Sozeau	2014-09-27
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
*	Renaming goal-entering functions.	Pierre-Marie Pédrot	2014-09-06
*	Moving the TacExtend node from atomic to plain tactics.	Pierre-Marie Pédrot	2014-08-18
*	Ring: prevent an error message to show in case of success.	Arnaud Spiwack	2014-08-05
*	Better fix of e5c025	Pierre Boutillier	2014-08-05
*	STM: VtQuery holds the id of the state it refers to	Carst Tankink	2014-08-04
*	Fix to make Coq compile, I think this should still be accepted.	Matthieu Sozeau	2014-08-03
*	Qualified ML tactic names. The plugin name is used to discriminate	Pierre-Marie Pédrot	2014-07-27
*	In generalized rewrite, avoid retyping completely and constantly the conclusi...	Matthieu Sozeau	2014-06-11
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	Fix extraction taking a type in the wrong environment.	Matthieu Sozeau	2014-05-06
*	Fix Field_tac to get fast reification again, with the fix on template univers...	Matthieu Sozeau	2014-05-06
*	Try a new way of handling template universe levels	Matthieu Sozeau	2014-05-06
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	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-05-06
*	Remove unused lookup table.	Guillaume Melquiond	2014-04-28
*	Removing useless try-with clauses in Goal.enter variants.	Pierre-Marie Pédrot	2014-04-25
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Less dependencies in Omega.	Pierre-Marie Pédrot	2014-02-08
*	Qed: feedback when type checking is done	Enrico Tassi	2013-12-24
*	Field_theory: nicer notations for constants 0 1 ...	Pierre Letouzey	2013-11-21
*	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