coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \|	Adding a universe argument to Pcoq.create_generic_entry.	Pierre-Marie Pédrot	2016-03-17
* \| \|	Relying on parsing rules rather than genarg to check if an argument is empty.	Pierre-Marie Pédrot	2016-03-17
* \| \|	Adopting the same rules for interpreting @, abbreviations and	Hugo Herbelin	2016-03-13
* \| \|	Supporting "(@foo) args" in patterns, where "@foo" has no arguments.	Hugo Herbelin	2016-03-13
* \| \|	Moving Autorewrite to Hightatctic.	Pierre-Marie Pédrot	2016-03-06
* \| \|	Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move.	Pierre-Marie Pédrot	2016-03-06
* \| \|	Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].	Pierre-Marie Pédrot	2016-03-04
* \| \|	Exchanging roles of tactic_arg and tactic_top_or_arg entries.	Pierre-Marie Pédrot	2016-03-04
* \| \|	Removing the UConstr entry of the tactic_arg AST.	Pierre-Marie Pédrot	2016-03-04
* \| \|	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
* \| \|	Uniformizing the parsing of argument scopes in Ltac.	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
* \| \|	Removing the METAIDENT token, as it is not used anymore.	Pierre-Marie Pédrot	2016-02-24
* \| \|	Removing the MetaIdArg entry of tactic expressions.	Pierre-Marie Pédrot	2016-02-24
* \| \|	Removing a source of type-unsafeness in Pcoq.	Pierre-Marie Pédrot	2016-02-02
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Implement support for universe binder lists in Instance and Program Fixpoint/...	Matthieu Sozeau	2016-01-23
* \| \|	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
\| * \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \| \|	Simplification and type-safety of Pcoq thanks to GADTs in Genarg.	Pierre-Marie Pédrot	2016-01-17
* \| \|	Temporary commit getting rid of Obj.magic unsafety for Genarg.	Pierre-Marie Pédrot	2016-01-17
* \| \|	Removing dynamic entries from Pcoq.	Pierre-Marie Pédrot	2016-01-17
* \| \|	ML extensions use untyped representation of user entries.	Pierre-Marie Pédrot	2016-01-17
* \| \|	Separating the parsing of user-defined entries from their intepretation.	Pierre-Marie Pédrot	2016-01-16
* \| \|	Less type-unsafety in Pcoq.	Pierre-Marie Pédrot	2016-01-16
\| * \|	Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.	Maxime Dénès	2016-01-15
* \| \|	Removing constr generic argument.	Pierre-Marie Pédrot	2016-01-14
* \| \|	Continuing 003fe3d5e on parsing positions.	Hugo Herbelin	2016-01-14
* \| \|	CLEANUP: removing unused field	Matej Kosik	2016-01-11
* \| \|	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