coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \|	Moving the Ltac definition command to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
* \| \|	Moving Print Ltac to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
* \| \|	Moving Tactic Notation to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
* \| \|	Moving Tacinterp to Hightactics.	Pierre-Marie Pédrot	2016-03-20
* \| \|	Fixing compilation with old versions of CAMLP5.	Pierre-Marie Pédrot	2016-03-19
* \| \|	Further reducing the dependencies of the EXTEND macros.	Pierre-Marie Pédrot	2016-03-19
* \| \|	Moving VernacSolve to an EXTEND-based definition.	Pierre-Marie Pédrot	2016-03-19
* \| \|	Moving the parsing of the Ltac proof mode to G_ltac.	Pierre-Marie Pédrot	2016-03-19
* \| \|	Moving the proof mode parsing management to Pcoq.	Pierre-Marie Pédrot	2016-03-19
* \| \|	Allowing generalized rules in typed symbols.	Pierre-Marie Pédrot	2016-03-19
* \| \|	Do not export entry_key from Pcoq anymore.	Pierre-Marie Pédrot	2016-03-19
* \| \|	Simplifying the code of Entry.	Pierre-Marie Pédrot	2016-03-19
* \| \|	Removing dead code in Pcoq.	Pierre-Marie Pédrot	2016-03-18
* \| \|	Making the EXTEND macros almost self-contained.	Pierre-Marie Pédrot	2016-03-18
* \| \|	ARGUMENT EXTEND made of only one entry share the same grammar.	Pierre-Marie Pédrot	2016-03-18
* \| \|	Removing the special status of generic arguments defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
* \| \|	Code factorization in Pcoq.	Pierre-Marie Pédrot	2016-03-17
* \| \|	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