coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-28
\|\
\| *	Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"	Lionel Rieg	2015-06-26
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
\| *	Adding a test to check whether two tactic notations conflict.	Pierre-Marie Pédrot	2015-05-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
\| *	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
\| *	Fixing bug #4190.	Pierre-Marie Pédrot	2015-04-16
* \|	Merge branch 'v8.5' into trunk	Enrico Tassi	2015-03-30
\|\\|
\| *	Revert "Useless check when loading notations through import."	Pierre-Marie Pédrot	2015-03-24
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-11
\|\\|
\| *	Tactic Notation: use stable unique key for notations (Close: 3970)	Enrico Tassi	2015-02-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-10
\|\\|
\| *	Tactic Notation: use stable unique key for notations (Close: 3970)	Enrico Tassi	2015-02-04
\| *	Revert "Tactic Notation: use stable unique key for notations (Close: 3970)"	Enrico Tassi	2015-02-03
\| *	Tactic Notation: use stable unique key for notations (Close: 3970)	Enrico Tassi	2015-02-03
* \|	Embedding the index of the ML tactic entry in the Tacexpr AST.	Pierre-Marie Pédrot	2015-01-21
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Fixing CAMLP4 compilation.	Pierre-Marie Pédrot	2014-12-16
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Failing on unbound notation variable in notation level modifiers	Hugo Herbelin	2014-12-15
*	Now printing "now a keyword" only in verbose mode.	Hugo Herbelin	2014-10-17
*	Notation: option to attach extra pretty printing rules to notations	Enrico Tassi	2014-09-29
*	Additional entry tactic_arg in Print Grammar tactic.	Pierre-Marie Pédrot	2014-09-03
*	Getting rid of atomic tactics in Tacenv.	Pierre-Marie Pédrot	2014-08-31
*	Moving the TacExtend node from atomic to plain tactics.	Pierre-Marie Pédrot	2014-08-18
*	Qualified ML tactic names. The plugin name is used to discriminate	Pierre-Marie Pédrot	2014-07-27
*	Useless keeping of dirpath in tactic aliases.	Pierre-Marie Pédrot	2014-06-30
*	Fix the behaviour of ML tactic notations w.r.t. Imports by making them	Pierre-Marie Pédrot	2014-05-13
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Useless check when loading notations through import.	Pierre-Marie Pédrot	2014-03-01
*	Fixing printing of only_parsing notations.	Pierre-Marie Pédrot	2014-02-25
*	Notations can now accept dummy arguments. If ever a bound variable is not	Pierre-Marie Pédrot	2013-12-22
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-10
*	Revert the previous commit. It broke Coq compilation.	ppedrot	2013-11-09
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-09
*	Moving notation types into grammar rule.	ppedrot	2013-11-09
*	Cleaning and documenting Egramcoq.	ppedrot	2013-11-09
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	cList.index is now cList.index_f, same for index0	letouzey	2013-10-23
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23
*	enhance marshallable option for freeze (minor TODO in safe_typing)	gareuselesinge	2013-08-08
*	Replacing uses of association lists by maps in notations.	ppedrot	2013-08-03
*	More dynamic argument scopes	letouzey	2013-07-17
*	States: frozen states can hold closures	gareuselesinge	2013-05-06
*	Avoid a few overzealous "when Errors.noncritical"	letouzey	2013-03-17
*	Restrict (try...with...) to avoid catching critical exn (part 13)	letouzey	2013-03-13
*	More monomorphization.	ppedrot	2013-03-05
*	Actually adding backtrace handling.	ppedrot	2013-01-28