coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Adding a new Ltac generic argument for forced tactics returing unit.	Pierre-Marie Pédrot	2016-03-20
*	Removing the special status of generic entries defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
*	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-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Removing the special status of open_constr generic argument.	Pierre-Marie Pédrot	2015-12-28
* \|	Tentative API fix for tactic arguments to be fed to tclWITHHOLES.	Pierre-Marie Pédrot	2015-12-27
* \|	Changing the toplevel type of the int_or_var generic type to int.	Pierre-Marie Pédrot	2015-12-21
* \|	Removing the now useless genarg generic argument.	Pierre-Marie Pédrot	2015-12-21
\|/
*	grammar: export hypident	Enrico Tassi	2015-03-30
*	Update headers.	Maxime Dénès	2015-01-12
*	Lazy interpretation of patterns so that expressions such as "intros H H'/H"	Hugo Herbelin	2014-08-18
*	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin	2014-08-18
*	[uconstr]: use a closure instead of eager substitution.	Arnaud Spiwack	2014-08-06
*	Add a type of untyped term to Ltac's value.	Arnaud Spiwack	2014-07-29
*	Removing useless use of metaids in tactic AST.	Pierre-Marie Pédrot	2014-05-22
*	Closing bug #3260	Julien Forest	2014-04-14
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey	2014-03-02
*	Removing the useless pattern ident genarg.	Pierre-Marie Pédrot	2013-12-19
*	Getting rid of casted_open_constr. It was only used by the	Pierre-Marie Pédrot	2013-11-30
*	Removing the use of leveled tactics wit_tacticn. It is now handled	ppedrot	2013-07-02
*	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot	2013-06-21