coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
*	Extend definition of inductives to include subtyping info	Amin Timany	2017-06-16
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	Don't double up on periods in anomalies	Jason Gross	2017-06-02
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	Allow flexible anonymous universes in instances and sorts.	Gaetan Gilbert	2017-05-03
* \|	[location] Make location optional in Loc.located	Emilio Jesus Gallego Arias	2017-04-25
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\|/
*	Moving Universes to the engine/ folder.	Pierre-Marie Pédrot	2016-10-30
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-24
\|\
\| *	Merge branch 'bug5036' into v8.6	Matthieu Sozeau	2016-10-20
\| \|\
\| \| *	Fix bug #5036 autorewrite, sections and universes	Matthieu Sozeau	2016-10-20
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\\| \|
\| * \|	Merge remote-tracking branch 'github/pr/299' into v8.6	Maxime Dénès	2016-09-30
\| \|\ \
\| * \| \|	Fix bug #5036 autorewrite, sections and universes	Matthieu Sozeau	2016-09-29
\| \| \|/ \| \|/\|
\| \| *	Fix bug #4869, allow Prop, Set, and level names in constraints.	Matthieu Sozeau	2016-09-29
\| \|/
* \|	Revert "Merge remote-tracking branch 'github/pr/283' into trunk"	Maxime Dénès	2016-09-22
* \|	Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.	Maxime Dénès	2016-09-20
* \|	Stylistic improvements in intf/decl_kinds.mli.	Maxime Dénès	2016-09-20
* \|	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
* \|	Unify location handling of error functions.	Emilio Jesus Gallego Arias	2016-08-19
\|/
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Reuse the typing_flags datatype for inductives.	Pierre-Marie Pédrot	2016-06-18
*	Moving the typing_flags to the environment.	Pierre-Marie Pédrot	2016-06-18
*	Factorizing the uses of Declareops.safe_flags.	Pierre-Marie Pédrot	2016-06-16
*	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot	2016-06-16
\|\
\| *	Assume totality: dedicated type rather than bool	Arnaud Spiwack	2016-06-14
* \|	Univs: more robust Universe/Constraint decls #4816	Matthieu Sozeau	2016-06-13
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\ \
\| * \|	Fix bug #4503: mixing universe polymorphic and monomorphic	Matthieu Sozeau	2016-01-23
* \| \|	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
* \| \|	Remove some useless type declarations.	Guillaume Melquiond	2016-01-02
\|/ /
* \|	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau	2015-11-27
* \|	Add a way to get the right fix_exn in external vernacular commands	Matthieu Sozeau	2015-10-30
* \|	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi	2015-10-28
* \|	Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names	Matthieu Sozeau	2015-10-27
* \|	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 Universe vernacular, fix bug #4287.	Matthieu Sozeau	2015-10-02
\| *	Propagate `Guarded` flag from syntax to kernel.	Arnaud Spiwack	2015-09-25
* \|	Hopefully better names to constructors of internal_flag, as discussed	Hugo Herbelin	2015-09-23
\| *	Add a corresponding field in `mutual_inductive_entry` (part 1).	Arnaud Spiwack	2015-06-24
\|/
*	Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior	Enrico Tassi	2015-02-14
*	Fix bug when discharging universe constraints coming from variables	Matthieu Sozeau	2015-01-13
*	Update headers.	Maxime Dénès	2015-01-12
*	kernel/ind Change interface of declare_mind and declare_mutual	Matthieu Sozeau	2015-01-05