coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	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
*	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
*	Hopefully better names to constructors of internal_flag, as discussed	Hugo Herbelin	2015-09-23
*	Nametab: print debug notice only in debug mode.	Maxime Dénès	2015-09-20
*	Add an if_verbose for "Fetching opaque proofs ..."	mlasson	2015-09-03
*	Fixing anomaly #3743 while printing an error message involving evar constraints.	Hugo Herbelin	2015-07-16
*	Option -type-in-type: added support in checker and making it contaminating	Hugo Herbelin	2015-07-10
*	Native compiler: refactor code handling pre-computed values.	Maxime Dénès	2015-07-10