coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing OCaml deprecated function names from the Lazy module.	Pierre-Marie Pédrot	2016-03-10
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-09
\|\
\| *	Adding backtraces to scheme error messages.	Pierre-Marie Pédrot	2016-03-07
* \|	Moving Autorewrite to Hightatctic.	Pierre-Marie Pédrot	2016-03-06
* \|	Removing dependency of Himsg in tactic files.	Pierre-Marie Pédrot	2016-03-06
* \|	Moving Tactic_debug to tactics/ folder.	Pierre-Marie Pédrot	2016-03-06
* \|	Moving Ltac traces to Tacexpr and Tacinterp.	Pierre-Marie Pédrot	2016-03-06
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\\|
\| *	Rename Ephemeron -> CEphemeron.	Maxime Dénès	2016-03-04
* \|	Moving the "clear" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
* \|	Printing notations: Cleaning in anticipation of fixing #4592.	Hugo Herbelin	2016-02-28
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-21
\|\\|
\| *	Fixing bug #4580: [Set Refine Instance Mode] also used for Program Instance.	Pierre-Marie Pédrot	2016-02-19
* \|	Renaming variants of Entries.local_entry	Matej Kosik	2016-02-16
* \|	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\ \
* \| \|	Using monotonic types for conversion functions.	Pierre-Marie Pédrot	2016-02-15
* \| \|	Moving conversion functions to the new tactic API.	Pierre-Marie Pédrot	2016-02-15
* \| \|	Renaming functions in Typing to stick to the standard e_* scheme.	Pierre-Marie Pédrot	2016-02-15
* \| \|	Monotonizing the Evarutil module.	Pierre-Marie Pédrot	2016-02-15
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\|\ \ \ \| \| \|/ \| \|/\|
\| \| *	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\| \|/ \|/\|
\| *	Improving error message with missing patterns in the presence of	Hugo Herbelin	2016-02-08
* \|	Infering atomic ML entries from their grammar.	Pierre-Marie Pédrot	2016-02-01
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\|
\| *	Fixing bug #3826: "Incompatible module types" is uninformative.	Pierre-Marie Pédrot	2016-01-24
\| *	Fixing bug #4495: Failed assertion in metasyntax.ml.	Pierre-Marie Pédrot	2016-01-24
\| *	Implement support for universe binder lists in Instance and Program Fixpoint/...	Matthieu Sozeau	2016-01-23
\| *	Restore warnings produced by the interpretation of the command line	Hugo Herbelin	2016-01-22
* \|	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
* \|	Removing dynamic entries from Pcoq.	Pierre-Marie Pédrot	2016-01-17
* \|	Tactic notation printing accesses all the token data.	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
* \|	CLEANUP: removing unused field	Matej Kosik	2016-01-11
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Remove deprecated command-line options such as "-as".	Guillaume Melquiond	2016-01-06
* \| \|	Reduce dependencies of interface files.	Guillaume Melquiond	2016-01-02
* \| \|	Remove useless rec flags.	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
* \| \|	Merge branch 'v8.5' into trunk	Guillaume Melquiond	2015-12-31
\|\ \ \ \| \| \|/ \| \|/\|
* \| \|	External tactics and notations now accept any tactic argument.	Pierre-Marie Pédrot	2015-12-30
* \| \|	Do not compose "str" and "to_string" whenever possible.	Guillaume Melquiond	2015-12-22
\| \|/ \|/\|
\| *	Inclusion of functors with restricted signature is now forbidden (fix #3746)	Pierre Letouzey	2015-12-22
* \|	CLEANUP: Vernacexpr.VernacDeclareTacticDefinition	Matej Kosik	2015-12-18
* \|	CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...	Matej Kosik	2015-12-18
* \|	CLEANUP: simplifying "Coqtop.init_gc" implementation	Matej Kosik	2015-12-18
* \|	CLEANUP: removing unnecessary wrapper function	Matej Kosik	2015-12-18