coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Improve semantics of -native-compiler flag.	Maxime Dénès	2015-07-09
*	Univs/minimization: Fix unused variable bug.	Matthieu Sozeau	2015-07-07
*	Assumptions: more informative print for False axiom (Close: #4054)	Enrico Tassi	2015-06-29
*	Fix bug #4254 with the help of J.H. Jourdan	Matthieu Sozeau	2015-06-26
*	Wrapped the declare_object function to pretty-print anomalies at loading time.	Thomas Sibut-Pinote	2015-06-25
*	On-demand Require.	Pierre-Marie Pédrot	2015-06-24
*	Splitting the library representation on disk in two.	Pierre-Marie Pédrot	2015-06-24