coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \|	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
\| \| * \|	More uniformity in the style of comparison functions.	Arnaud Spiwack	2015-10-30
\| \| * \|	Make the code of compare functions linear in the number of constructors.	Arnaud Spiwack	2015-10-29
* \| \| \|	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
* \|	Unexport Loadpath.get_paths.	Guillaume Melquiond	2015-09-30
* \|	Fix dumb typo.	Guillaume Melquiond	2015-09-29
* \|	Make the interface of System.raw_extern_intern much saner.	Guillaume Melquiond	2015-09-29
* \|	Prevent States.intern_state and System.extern_intern from looking up files in...	Guillaume Melquiond	2015-09-29
* \|	Remove some uses of Loadpath.get_paths.	Guillaume Melquiond	2015-09-29
* \|	Make -load-vernac-object respect the loadpath.	Guillaume Melquiond	2015-09-28
\| *	Show assumptions of well-foundedness in `Print Assumptions`	Arnaud Spiwack	2015-09-25
* \|	The -require option now accepts a logical path instead of a physical one.	Pierre-Marie Pédrot	2015-09-25
* \|	The -compile option now accepts ".v" files and outputs a warning otherwise.	Pierre-Marie Pédrot	2015-09-25
\| *	Propagate `Guarded` flag from syntax to kernel.	Arnaud Spiwack	2015-09-25