coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	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
* \|	Removing useless grammar.cma dependencies.	Pierre-Marie Pédrot	2016-03-06
* \|	Moving Eauto to a simple ML file.	Pierre-Marie Pédrot	2016-03-06
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\\|
* \|	Exporting build_selector, a component of discriminate, for use in congruence.	Hugo Herbelin	2016-03-05
* \|	Adding some standard arguments in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
* \|	Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].	Pierre-Marie Pédrot	2016-03-04
* \|	Removing the UConstr entry of the tactic_arg AST.	Pierre-Marie Pédrot	2016-03-04
* \|	Moving the "move" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
* \|	Moving the "exists" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
* \|	Moving the "symmetry" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
* \|	Moving the "generalize dependent" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
* \|	Moving the "clearbody" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
* \|	Moving the "clear" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
* \|	Moving the "cofix" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
* \|	Moving the "fix" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
\| *	Fixing bug #4596: [rewrite] broke in the past few weeks.	Pierre-Marie Pédrot	2016-02-28
* \|	Removing Tacmach.New qualification in Tacinterp.	Pierre-Marie Pédrot	2016-02-27
* \|	Removing some compatibility layers in Tacinterp.	Pierre-Marie Pédrot	2016-02-27
* \|	Removing the MetaIdArg entry of tactic expressions.	Pierre-Marie Pédrot	2016-02-24
* \|	Getting rid of the "<:tactic< ... >>" quotations.	Pierre-Marie Pédrot	2016-02-24
* \|	Moving tauto.ml4 to a proper ML file.	Pierre-Marie Pédrot	2016-02-23
\| *	Fix bug #4544: Backtrack on using full betaiota reduction during keyed unific...	Matthieu Sozeau	2016-02-23
* \|	Moving the Tauto tactic to proper Ltac.	Pierre-Marie Pédrot	2016-02-22
* \|	The tactic generic argument now returns a value rather than a glob_expr.	Pierre-Marie Pédrot	2016-02-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-21
\|\\|
\| *	Fix regression from 8.4 in reflexivity/...	Matthieu Sozeau	2016-02-19
* \|	FIX: of my previous merging mistake	Matej Kosik	2016-02-18