coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
*	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
*	CLEANUP: Vernacexpr.vernac_expr	Matej Kosik	2015-12-18
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-15
\|\
\| *	Flag -compat 8.4 now loads Coq.Compat.Coq84.	Maxime Dénès	2015-12-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\|
\| *	Print Assumptions: improve detection of case on an axiom of False	Enrico Tassi	2015-12-09
* \|	Moving extended_rel_vect/extended_rel_list to the kernel.	Hugo Herbelin	2015-12-05
* \|	Moving three related small half-general half-ad-hoc utility functions	Hugo Herbelin	2015-12-05
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\\|
\| *	Univs/Program: update the universe context with global universe	Matthieu Sozeau	2015-12-02
\| *	Fix bug #4444: Next Obligation performed after a Section opening was	Matthieu Sozeau	2015-12-02
* \|	Removing dead code in Obligations.	Pierre-Marie Pédrot	2015-12-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Univs: correctly register universe binders for lemmas.	Matthieu Sozeau	2015-11-28
\| *	Fix [Polymorphic Hint Rewrite].	Matthieu Sozeau	2015-11-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-26
\|\\|
\| *	Univs: carry on universe substitution when defining obligations of	Matthieu Sozeau	2015-11-24
\| *	Fix output of universe arcs. (Fix bug #4422)	Guillaume Melquiond	2015-11-23
\| *	Univs: generation of induction schemes should not generated useless	Matthieu Sozeau	2015-11-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\\|
\| *	Allow program hooks to see the refined universe_context at the end of a	Matthieu Sozeau	2015-11-19
* \|	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
\|\\|
\| *	Command.declare_definition: grab the fix_exn early (follows 77cf18e)	Enrico Tassi	2015-10-30
\| *	Add a way to get the right fix_exn in external vernacular commands	Matthieu Sozeau	2015-10-30
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\\|
\| *	Accept option -compat 8.5. (Fix bug #4393)	Guillaume Melquiond	2015-10-29
\| *	Univs: local names handling.	Matthieu Sozeau	2015-10-28
\| *	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi	2015-10-28
\| *	Univs: fix bug #4375, accept universe binders on (co)-fixpoints	Matthieu Sozeau	2015-10-28
\| *	Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names	Matthieu Sozeau	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
* \|	Indexing existentially quantified entries returned by interp_entry_name.	Pierre-Marie Pédrot	2015-10-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-26
\|\\|
\| *	Minor module cleanup : error HigherOrderInclude was never happening	Pierre Letouzey	2015-10-25
* \|	Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.	Pierre-Marie Pédrot	2015-10-21
* \|	Boxing the Goal.enter primitive into a record type.	Pierre-Marie Pédrot	2015-10-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\\|
* \|	Constraining refine to monotonic functions.	Pierre-Marie Pédrot	2015-10-18
\| *	Miscellaneous typos, spacing, US spelling in comments or variable names.	Hugo Herbelin	2015-10-18
* \|	Clarifying and documenting the UState API.	Pierre-Marie Pédrot	2015-10-17
\| *	Lemmas accept the Local flag.	Pierre-Marie Pédrot	2015-10-17
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Remove -vm flag of coqtop.	Maxime Dénès	2015-10-14