coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)	Pierre Letouzey	2016-07-03
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
*	Removing tactic compatibility layers in setoid_ring.	Pierre-Marie Pédrot	2016-06-24
*	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
*	Adding printers for ring and field commands.	Hugo Herbelin	2016-06-16
*	Remove inappropriate comment.	Maxime Dénès	2016-06-16
*	Merge remote-tracking branch 'github/evarunsafe' into trunk	Matthieu Sozeau	2016-06-14
\|\
\| *	newring: fix for hack using evars as integers.	Matthieu Sozeau	2016-06-09
* \|	Compilation via pack for plugins of the stdlib	Pierre Letouzey	2016-06-08
\|/
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Moving the Val module to Geninterp.	Pierre-Marie Pédrot	2016-05-04
*	Revert "Adding printers for ring and field commands."	Hugo Herbelin	2016-04-27
*	Adding printers for ring and field commands.	Hugo Herbelin	2016-04-27
*	Getting rid of the "_mods" parsing entry.	Pierre-Marie Pédrot	2016-04-01
*	Removing the special status of generic entries defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
*	Removing useless grammar.cma dependencies.	Pierre-Marie Pédrot	2016-03-06
*	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
*	The tactic generic argument now returns a value rather than a glob_expr.	Pierre-Marie Pédrot	2016-02-22
*	Moving conversion functions to the new tactic API.	Pierre-Marie Pédrot	2016-02-15
*	Renaming functions in Typing to stick to the standard e_* scheme.	Pierre-Marie Pédrot	2016-02-15
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	External tactics and notations now accept any tactic argument.	Pierre-Marie Pédrot	2015-12-30
* \|	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