coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	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
*	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
\| *	Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").	Pierre-Marie Pédrot	2016-02-17
* \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-17
\|\ \
* \| \|	Tacticals: typo in a comment	Pierre Letouzey	2016-02-16
\| * \|	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|/\| \|
* \| \|	Using monotonic types for conversion functions.	Pierre-Marie Pédrot	2016-02-15
* \| \|	Code factorization of tactic "unfold_body".	Pierre-Marie Pédrot	2016-02-15
* \| \|	More conversion functions in the new tactic API.	Pierre-Marie Pédrot	2016-02-15
* \| \|	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
* \| \|	Monotonizing the Evarutil module.	Pierre-Marie Pédrot	2016-02-15
\| * \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\|/ /
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\|
\| *	Fix bug #4537: Coq 8.5 is slower in typeclass resolution.	Pierre-Marie Pédrot	2016-01-27
\| *	Fixing bug #4511: evar tactic can create non-typed evars.	Pierre-Marie Pédrot	2016-01-24
\| *	Implement support for universe binder lists in Instance and Program Fixpoint/...	Matthieu Sozeau	2016-01-23
* \|	Fixing a use of "clear" on an non-existing hypothesis in intro-patterns.	Hugo Herbelin	2016-01-22
* \|	New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).	Hugo Herbelin	2016-01-21
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
* \|	Stronger invariants on the use of the introduction pattern (pat1,...,patn).	Hugo Herbelin	2016-01-21
* \|	Fixing some problems with double induction.	Hugo Herbelin	2016-01-21
* \|	Code simplification in elim.ml.	Hugo Herbelin	2016-01-20
* \|	Fixing a bug with introduction patterns over inductive types containing let-ins.	Hugo Herbelin	2016-02-18
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| *	Fix bug #4420: check_types was losing universe constraints.	Matthieu Sozeau	2016-01-19
* \|	Moving val_cast to Tacinterp.	Pierre-Marie Pédrot	2016-01-17
* \|	Getting rid of the awkward unpack mechanism from Genarg.	Pierre-Marie Pédrot	2016-01-17
* \|	Removing constr generic argument.	Pierre-Marie Pédrot	2016-01-14
* \|	Removing ident and var generic arguments.	Pierre-Marie Pédrot	2016-01-14
* \|	Moving is_quantified_hypothesis to new proof engine.	Hugo Herbelin	2016-01-14
* \|	Update in the documentation of parts of the code of destruct/induction.	Hugo Herbelin	2016-01-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\\|
\| *	Fix essential bug in new Keyed Unification mode reported by R. Krebbers.	Matthieu Sozeau	2016-01-12
* \|	CLEANUP: removing unused field	Matej Kosik	2016-01-11
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
\| \| *	Fix bug #3338 again, no progress is necessary for the success of rewrite_strat.	Matthieu Sozeau	2016-01-11