coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Normalizing the names of dynamic types to follow a typ_* scheme.	Pierre-Marie Pédrot	2016-05-04
*	Removing external uses of Val.inject and making Geninterp.interp return Val.t	Pierre-Marie Pédrot	2016-05-04
*	Removing the Value.of_* API for parameterized types.	Pierre-Marie Pédrot	2016-05-04
*	Moving the Val module to Geninterp.	Pierre-Marie Pédrot	2016-05-04
*	Getting rid of the Geninterp.generic_interp function.	Pierre-Marie Pédrot	2016-05-04
*	Switching to an untyped toplevel representation for Ltac values.	Pierre-Marie Pédrot	2016-05-04
*	Moving Ftactic and Geninterp to the engine folder.	Pierre-Marie Pédrot	2016-05-04
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\
\| *	In Regular Subst Tactic mode, ensure that the order of hypotheses is	Hugo Herbelin	2016-05-03
\| *	Fix bug #4707: clearbody much slower in 8.5pl1.	Pierre-Marie Pédrot	2016-05-03
* \|	Revert "In the short term, stronger invariant on the syntax of TacAssert, what"	Hugo Herbelin	2016-04-27
* \|	In the short term, stronger invariant on the syntax of TacAssert, what	Hugo Herbelin	2016-04-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-09
\|\\|
\| *	Allow to unset the refinement mode of Instance in ML	Matthieu Sozeau	2016-04-07
\| *	Fixing an incorrect use of prod_appvect on a term which was not a	Hugo Herbelin	2016-04-07
\| *	Fixing the "No applicable tactic" non informative error message	Hugo Herbelin	2016-04-03
* \|	Moving Autorewrite back to tactics/.	Pierre-Marie Pédrot	2016-03-25
* \|	Moving Eqdecide to tactics/.	Pierre-Marie Pédrot	2016-03-25
* \|	Moving Eauto and Class_tactics to tactics/.	Pierre-Marie Pédrot	2016-03-25
* \|	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot	2016-03-21
* \|	Moving Tacsubst to hightactics.	Pierre-Marie Pédrot	2016-03-20
* \|	Relying on generic arguments to represent Extern hints.	Pierre-Marie Pédrot	2016-03-20
* \|	Adding a new Ltac generic argument for forced tactics returing unit.	Pierre-Marie Pédrot	2016-03-20
* \|	Moving Tacenv to Hightactics.	Pierre-Marie Pédrot	2016-03-20
* \|	Moving Tactic_debug to Hightactic.	Pierre-Marie Pédrot	2016-03-20
* \|	Making Evarutil independent from Reductionops.	Pierre-Marie Pédrot	2016-03-20
* \|	Moving Refine to its proper module.	Pierre-Marie Pédrot	2016-03-20
* \|	Making Proofview independent of Logic.	Pierre-Marie Pédrot	2016-03-20
* \|	Fixing the classification of Tactic Notation.	Pierre-Marie Pédrot	2016-03-20
\| *	Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4.	Pierre-Marie Pédrot	2016-03-20
* \|	Moving Tacintern to Hightactics.	Pierre-Marie Pédrot	2016-03-20
* \|	Moving the Ltac definition command to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
* \|	Moving the tactic related code from Metasyntax to a new file.	Pierre-Marie Pédrot	2016-03-20
* \|	Moving Print Ltac to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
* \|	Moving Tactic Notation to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
* \|	Moving Tacinterp to Hightactics.	Pierre-Marie Pédrot	2016-03-20
* \|	Moving the use of Tactic_option from Obligations to G_obligations.	Pierre-Marie Pédrot	2016-03-19
* \|	Removing the special status of generic arguments defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
* \|	Removing the special status of generic entries defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
* \|	Adding a universe argument to Pcoq.create_generic_entry.	Pierre-Marie Pédrot	2016-03-17
* \|	Removing the registering of default values for generic arguments.	Pierre-Marie Pédrot	2016-03-17
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-09
\|\\|
* \|	Redo fix init_setoid -> init_relation_classes	Matthieu Sozeau	2016-03-09
\| *	Fix strategy of Keyed Unification	Matthieu Sozeau	2016-03-09
* \|	Moving Autorewrite to Hightatctic.	Pierre-Marie Pédrot	2016-03-06
* \|	Putting Tactic_debug just below Tacinterp.	Pierre-Marie Pédrot	2016-03-06
* \|	Removing dependency of Himsg in tactic files.	Pierre-Marie Pédrot	2016-03-06
* \|	Moving Tactic_debug to tactics/ folder.	Pierre-Marie Pédrot	2016-03-06
* \|	Moving Ltac traces to Tacexpr and Tacinterp.	Pierre-Marie Pédrot	2016-03-06