coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| *	Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.	Maxime Dénès	2016-01-15
* \|	Changing "P is assumed" to "P is declared".	Hugo Herbelin	2016-01-14
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-06
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Protect code against changes in Map interface.	Maxime Dénès	2016-01-06
* \| \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
* \| \|	Remove keys for evar and meta, since they cannot occur.	Guillaume Melquiond	2016-01-02
* \| \|	Remove some useless type declarations.	Guillaume Melquiond	2016-01-02
* \| \|	Remove Library.mem, which is pointless since 8.5.	Guillaume Melquiond	2015-12-31
* \| \|	Avoid a pointless conversion/copy.	Guillaume Melquiond	2015-12-22
* \| \|	Do not compose "str" and "to_string" whenever possible.	Guillaume Melquiond	2015-12-22
* \| \|	Move the From logic to Loadpath.expand_path.	Guillaume Melquiond	2015-12-22
* \| \|	Do not query module files that have already been loaded.	Guillaume Melquiond	2015-12-22
\| \|/ \|/\|
* \|	COMMENTS: added to some variants of "Globalnames.global_reference" type.	Matej Kosik	2015-12-18
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\\|
* \|	Leveraging GADTs to provide a better Dyn API.	Pierre-Marie Pédrot	2015-12-05
* \|	Specializing the Dyn module to each usecase.	Pierre-Marie Pédrot	2015-12-04
\| *	Univs: fix bug #4443.	Matthieu Sozeau	2015-12-03
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau	2015-11-27
\| *	Avoid recording spurious Set <= Top.i constraints which are always	Matthieu Sozeau	2015-11-27
* \|	More efficient implementation of equality-up-to-universes in Universes.	Pierre-Marie Pédrot	2015-11-26
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-26
\|\\|
* \|	More invariants in UState.	Pierre-Marie Pédrot	2015-11-26
\| *	Univs: fix type_of_global_in_context not returning instantiated universe cont...	Matthieu Sozeau	2015-11-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	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
\|\\|
\| *	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
\| *	lib_stack: API to reorder the libstack	Enrico Tassi	2015-10-28
\| *	Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names	Matthieu Sozeau	2015-10-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-26
\|\\|
\| *	Declaremods: replace two anomalies by user errors (fix #3974 and #3975)	Pierre Letouzey	2015-10-25
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	Univs: fix bug #3807	Matthieu Sozeau	2015-10-08
\| *	Goptions: new value type: optional string	Enrico Tassi	2015-10-08
* \|	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot	2015-10-06
\|/
*	Univs: Change intf of push_named_def to return the computed universe	Matthieu Sozeau	2015-10-02
*	Univs: refined handling of assumptions	Matthieu Sozeau	2015-10-02
*	Univs: fix minimization to allow lowering a universe to Set, not Prop.	Matthieu Sozeau	2015-10-02
*	Univs: fix Universe vernacular, fix bug #4287.	Matthieu Sozeau	2015-10-02
*	Univs: minimization, adapt to graph invariants.	Matthieu Sozeau	2015-10-02
*	Forcing i > Set for global universes (incomplete)	Matthieu Sozeau	2015-10-02
*	Universes: enforce Set <= i for all Type occurrences.	Matthieu Sozeau	2015-10-02