coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Cleanup code according to comments.	Matthieu Sozeau	2016-10-20
*	Fix minimization to be insensitive to redundant arcs.	Matthieu Sozeau	2016-10-20
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	universes.ml: Minor code cleanup	Matthieu Sozeau	2016-06-29
*	Univs: more robust Universe/Constraint decls #4816	Matthieu Sozeau	2016-06-13
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\|\
\| *	Optimizing the universes_of_constr_function.	Pierre-Marie Pédrot	2016-02-03
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\\|
\| *	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
* \|	More invariants in UState.	Pierre-Marie Pédrot	2015-11-26
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\\|
\| *	Univs: local names handling.	Matthieu Sozeau	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-09
\|\\|
\| *	Univs: fix bug #3807	Matthieu Sozeau	2015-10-08
* \|	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot	2015-10-06
\|/
*	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: 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
*	Univs/minimization: Fix unused variable bug.	Matthieu Sozeau	2015-07-07
*	Fix bug #4254 with the help of J.H. Jourdan	Matthieu Sozeau	2015-06-26
*	Fix bug #3446.	Matthieu Sozeau	2015-06-11
*	Fix bug #4159	Matthieu Sozeau	2015-05-27
*	Tactical `progress` compares term up to potentially equalisable universes.	Arnaud Spiwack	2015-04-22
*	Strengthen minimization: it shouldn't set a universe u to a max if it	Matthieu Sozeau	2015-04-09
*	Refactoring in [Constr].	Arnaud Spiwack	2015-02-24
*	Univs: proper printing of global and local universe names (only	Matthieu Sozeau	2015-01-17
*	Update headers.	Maxime Dénès	2015-01-12
*	Pass around information on the use of template polymorphism for	Matthieu Sozeau	2014-11-23
*	Universes.nf_evars_and_universes_opt_subst substitutes evars eagerly.	Pierre-Marie Pédrot	2014-11-10
*	library/opaqueTables: enable their use in interactive mode	Enrico Tassi	2014-10-13
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Make eq_pattern_test/eq_test work up to the equivalence of primitive	Matthieu Sozeau	2014-09-24
*	Fix computation of dangling constraints at the end of a proof (bug #3531).	Matthieu Sozeau	2014-08-25
*	instanciation is French, instantiation is English	Jason Gross	2014-08-25
*	Small code simplification.	Pierre-Marie Pédrot	2014-08-05
*	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau	2014-08-03
*	More straightforward definition of Universes.add_list_map.	Pierre-Marie Pédrot	2014-07-21
*	Cleanup substitution inside universe instances, only done through subst_fn now,	Matthieu Sozeau	2014-07-21
*	Cleanup code related to the constraint solving, which sits now outside the	Matthieu Sozeau	2014-07-03
*	Add toplevel commands to declare global universes and constraints.	Matthieu Sozeau	2014-07-01
*	Fixed some HoTT bugs, provide a proper error message when giving an ill-formed	Matthieu Sozeau	2014-06-20