coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\
\| *	Merge remote-tracking branch 'github/pr/232' into v8.6	Maxime Dénès	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
* \| \|	Moving the tactic-in-term extension from G_constr to G_ltac.	Pierre-Marie Pédrot	2016-09-14
* \| \|	Move Ltac-specific components from G_proofs to G_ltac.	Pierre-Marie Pédrot	2016-09-11
* \| \|	Making Vernacexpr independent from Tacexpr.	Pierre-Marie Pédrot	2016-09-08
* \| \|	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
* \| \|	Unify location handling of error functions.	Emilio Jesus Gallego Arias	2016-08-19
\|/ /
* \|	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
\| *	Goal selectors now use the keyword [only].	Cyprien Mangin	2016-06-30
\|/
*	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
*	par: like all: but in parallel	Enrico Tassi	2016-06-17
*	Typo in comment.	Hugo Herbelin	2016-06-16
*	Fixing parsing of constr argument of ltac functions at level 8 in the	Hugo Herbelin	2016-06-16
*	Merge 'pr/191' into trunk	Enrico Tassi	2016-06-16
\|\
\| *	Ident selectors cannot be used inside an Ltac expression.	Cyprien Mangin	2016-06-14
\| *	Goal selectors are now tacticals and can be used as such.	Cyprien Mangin	2016-06-14
\| *	Remove the need for brackets in goal selectors.	Cyprien Mangin	2016-06-14
\| *	Fix usage of Pervasives in goal selectors.	Cyprien Mangin	2016-06-14
\| *	Fix the pretty-printing of goal range selectors.	Cyprien Mangin	2016-06-14
\| *	Add goal range selectors.	Cyprien Mangin	2016-06-14
* \|	STM: proof block detection for par:	Enrico Tassi	2016-06-06
* \|	STM: proof block detection/error resilience API	Enrico Tassi	2016-06-06
\|/
*	Adding the Print Ltac Signature command.	Pierre-Marie Pédrot	2016-06-05
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Removing the Entry module now that rules need not be marshalled.	Pierre-Marie Pédrot	2016-05-10
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Revert "Fixing parsing of constr argument of ltac functions at level 8 in the"	Hugo Herbelin	2016-04-27
*	Revert "Typo in comment."	Hugo Herbelin	2016-04-27
*	Typo in comment.	Hugo Herbelin	2016-04-27
*	Fixing parsing of constr argument of ltac functions at level 8 in the	Hugo Herbelin	2016-04-27
*	Higher-level API for tactic notations.	Pierre-Marie Pédrot	2016-04-24
*	Moving and enhancing the grammar_tactic_prod_item_expr type.	Pierre-Marie Pédrot	2016-04-14
*	Removing extra spaces in printing arguments of VERNAC EXTEND.	Hugo Herbelin	2016-04-09
*	Re-add printer for tacdef_body so that Ltac definitions are printed by pr_ver...	Hugo Herbelin	2016-04-09
*	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot	2016-03-21