coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Prevent user-defined ring morphisms from ever being evaluated.	Guillaume Melquiond	2017-05-09
*	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
*	Remove some unused values and types	Gaetan Gilbert	2017-04-27
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|\
\| *	Mark ring morphisms as opaque.	Guillaume Melquiond	2017-03-22
\| *	Change the parser and printer so that they use IZR for real constants.	Guillaume Melquiond	2017-03-22
\| *	Fix broken evaluation strategies for ring and field.	Guillaume Melquiond	2017-03-22
\| *	Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun	Maxime Dénès	2017-03-14
\| \|\
\| * \|	Moving the Ltac plugin to a pack-based one.	Pierre-Marie Pédrot	2017-02-17
\| \| *	[cleanup] Change Id.t option to Name.t in TacFun	Tej Chajed	2017-02-16
\| \|/
* \|	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
* \|	Removing compatibility layers related to printing.	Pierre-Marie Pédrot	2017-02-14
* \|	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Removing compatibility layers in Retyping	Pierre-Marie Pédrot	2017-02-14
* \|	Removing some return type compatibility layers in Termops.	Pierre-Marie Pédrot	2017-02-14
* \|	Setoid_ring API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Quote API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Reductionops now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Rewrite API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Goal API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Typing API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Retyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|/
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\
\| *	Ncring_initial: avoid a notation overriding	Pierre Letouzey	2016-09-29
\| *	Ring_theory: avoid overriding a few notations	Pierre Letouzey	2016-09-28
* \|	Merging Stdarg and Constrarg.	Pierre-Marie Pédrot	2016-09-21
* \|	Moving Ltac-specific generic arguments to their own file in the ltac/ folder.	Pierre-Marie Pédrot	2016-09-15
* \|	Moving Ltac-specific parsing API to ltac/ folder.	Pierre-Marie Pédrot	2016-09-14
* \|	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
* \|	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
\|/
*	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