coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove some useless type declarations.	Guillaume Melquiond	2016-01-02
*	Simplification of grammar_prod_item type.	Pierre-Marie Pédrot	2016-01-02
*	Separation of concern in TacAlias API.	Pierre-Marie Pédrot	2016-01-02
*	External tactics and notations now accept any tactic argument.	Pierre-Marie Pédrot	2015-12-30
*	Removing unused parsing entries.	Pierre-Marie Pédrot	2015-12-28
*	Removing the special status of open_constr generic argument.	Pierre-Marie Pédrot	2015-12-28
*	Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.ml	Hugo Herbelin	2015-12-25
*	Fixing non exhaustive pattern-matching in 003fe3d5e60b.	Hugo Herbelin	2015-12-25
*	Removing auto from the tactic AST.	Pierre-Marie Pédrot	2015-12-24
*	Partial backtrack on commit 20641795624.	Pierre-Marie Pédrot	2015-12-23
*	CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified	Matej Kosik	2015-12-18
*	CLEANUP: Vernacexpr.VernacDeclareTacticDefinition	Matej Kosik	2015-12-18
*	ALPHA-CONVERSION: in "parsing/g_vernac.ml4" file	Matej Kosik	2015-12-18
*	CLEANUP: Vernacexpr.vernac_expr	Matej Kosik	2015-12-18
*	Adding a token "index" representing positions (1st, 2nd, etc.).	Hugo Herbelin	2015-12-15
*	Tactics: Generalizing the use of the experimental clearing modifier to	Hugo Herbelin	2015-12-15
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\
\| *	Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.	Hugo Herbelin	2015-12-10
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\\|
\| *	Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)	Hugo Herbelin	2015-12-05
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\\|
\| *	Improving syntax of pat/constr introduction pattern so that	Hugo Herbelin	2015-12-02
\| *	Dead code from August 2014 in apply in.	Hugo Herbelin	2015-12-02
\| *	Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.	Hugo Herbelin	2015-12-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Fixing the "parsing rules with idents later declared as keywords" problem.	Hugo Herbelin	2015-11-26
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\|
\| *	Adding syntax "Show id" to show goal named id (shelved or not).	Hugo Herbelin	2015-11-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-30
\|\\|
\| *	Manually expand red_tactic so that notations do not break reduction tactics. ...	Guillaume Melquiond	2015-10-30
\| *	Manually expand the debugging versions of "trivial" and "auto". (Fix bug #4392)	Guillaume Melquiond	2015-10-29
* \|	Fixing the return type of the Atoken symbol.	Pierre-Marie Pédrot	2015-10-28
* \|	Removing unused code in Pcoq.	Pierre-Marie Pédrot	2015-10-27
* \|	Type-safe Egramml.grammar_prod_item.	Pierre-Marie Pédrot	2015-10-27
* \|	Finer type for Pcoq.interp_entry_name.	Pierre-Marie Pédrot	2015-10-27
* \|	Getting rid of most uses of unsafe_grammar_extend.	Pierre-Marie Pédrot	2015-10-27
* \|	Type-safe Egramml.make_rule.	Pierre-Marie Pédrot	2015-10-27
* \|	Indexing existentially quantified entries returned by interp_entry_name.	Pierre-Marie Pédrot	2015-10-27
* \|	Type-safe grammar extensions.	Pierre-Marie Pédrot	2015-10-27
* \|	Pcoq entries are given a proper module.	Pierre-Marie Pédrot	2015-10-26
* \|	Getting rid of the Atactic entry.	Pierre-Marie Pédrot	2015-10-25
* \|	Getting rid of the Agram entry.	Pierre-Marie Pédrot	2015-10-25
* \|	Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.	Pierre-Marie Pédrot	2015-10-21
* \|	Turn Pcoq into a regular ML file.	Pierre-Marie Pédrot	2015-10-21
* \|	Expanding the grammar extensions of Pcoq.	Pierre-Marie Pédrot	2015-10-21
* \|	Removing the dependencies of Pcoq in IFDEF macros.	Pierre-Marie Pédrot	2015-10-21
* \|	Expliciting some uses of Compat module.	Pierre-Marie Pédrot	2015-10-21
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Fix some typos.	Guillaume Melquiond	2015-10-14
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13