coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7080: Swapping Context and Constr and defining declarations on cons...	Maxime Dénès	2018-06-29
\|\
* \	Merge PR #7866: Implementation of mutual records in the higher strata	Maxime Dénès	2018-06-28
\|\ \
\| \| *	Swapping Context and Constr: defining declarations on constr in Constr.	Hugo Herbelin	2018-06-27
\| \|/ \|/\|
* \|	Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).	Hugo Herbelin	2018-06-26
\| *	Handle mutual records in upper layers.	Pierre-Marie Pédrot	2018-06-24
\|/
*	Using more general information for primitive records.	Pierre-Marie Pédrot	2018-06-23
*	Merge PR #7797: Remove reference name type.	Enrico Tassi	2018-06-19
\|\
\| *	Remove reference name type.	Maxime Dénès	2018-06-18
* \|	Remove the proj_eta field of the kernel.	Pierre-Marie Pédrot	2018-06-17
* \|	Remove special declaration of primitive projections in the kernel.	Pierre-Marie Pédrot	2018-06-17
\|/
*	[TYPO FIX] elimitate -> eliminate	Siddharth	2018-06-14
*	[api] Remove Misctypes.	Emilio Jesus Gallego Arias	2018-06-12
*	[api] Misctypes removal: move Tactypes to proofs	Emilio Jesus Gallego Arias	2018-06-12
*	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias	2018-06-12
*	[api] Misctypes removal: miscellaneous aliases.	Emilio Jesus Gallego Arias	2018-06-12
*	[api] Misctypes removal: module_kind to Declaremods	Emilio Jesus Gallego Arias	2018-06-12
*	Fixing #7700 (section variables bound to abbreviations were not found).	Hugo Herbelin	2018-06-10
*	Merge PR #7682: Fixes #7641: more detailed message about disjunctive patterns...	Emilio Jesus Gallego Arias	2018-06-03
\|\
\| *	Fixes #7641: more detailed message for disjunctive patterns with different vars.	Hugo Herbelin	2018-06-03
* \|	Fixes #7636: location missing on deprecated compatibility notations.	Hugo Herbelin	2018-06-02
\|/
*	[notations] Split interpretation and parsing of notations	Emilio Jesus Gallego Arias	2018-05-31
*	[api] Move `Constrexpr` to the `interp` module.	Emilio Jesus Gallego Arias	2018-05-31
*	[api] Remove deprecated objects in engine / interp / library	Emilio Jesus Gallego Arias	2018-05-30
*	[api] Remove deprecated object from `Term`	Emilio Jesus Gallego Arias	2018-05-30
*	Remove some occurrences of Evd.empty	Maxime Dénès	2018-05-25
*	Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...	Pierre-Marie Pédrot	2018-05-24
\|\
\| *	Moving Option.smart_map to Option.Smart.map.	Hugo Herbelin	2018-05-23
\| *	Collecting List.smart_* functions into a module List.Smart.	Hugo Herbelin	2018-05-23
\| *	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin	2018-05-23
* \|	[api] Move `Vernacexpr` to parsing.	Emilio Jesus Gallego Arias	2018-05-23
\|/
*	Merge PR #7384: Split Universes	Pierre-Marie Pédrot	2018-05-22
\|\
* \	Merge PR #6965: [api] Move universe syntax to `Glob_term`	Pierre-Marie Pédrot	2018-05-18
\|\ \
\| \| *	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert	2018-05-17
\| \| *	Split off Universes functions dealing with names.	Gaëtan Gilbert	2018-05-17
\| \|/ \|/\|
* \|	Fixing a bug in printing the body of a located notation.	Hugo Herbelin	2018-05-13
* \|	Removing a superfluous trailing newline in "Locate" for a notation.	Hugo Herbelin	2018-05-13
* \|	Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).	Hugo Herbelin	2018-05-10
* \|	Fixes part 1 of #7462 (only-printing not to override existing interp rule).	Hugo Herbelin	2018-05-10
\| *	[api] Move universe syntax to `Glob_term`	Emilio Jesus Gallego Arias	2018-05-08
\|/
*	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
*	[api] Relocate `intf` modules according to dependency-order.	Emilio Jesus Gallego Arias	2018-04-23
*	Merge PR #7231: Fixing the 3 cases of a "Stream.Error" ended with two periods.	Enrico Tassi	2018-04-13
\|\
* \	Merge PR #6972: [api] Deprecate a couple of aliases that we missed.	Maxime Dénès	2018-04-12
\|\ \
\| \| *	Fixing the 3 cases of a "Stream.Error" ended with two periods.	Hugo Herbelin	2018-04-12
\| \|/ \|/\|
* \|	Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while look...	Emilio Jesus Gallego Arias	2018-04-09
\|\ \
* \ \	Merge PR #7129: Fix #7124: Warning "Ignoring implicit status" does not provid...	Hugo Herbelin	2018-04-06
\|\ \ \
* \| \| \|	Refactor impargs code.	Jasper Hugunin	2018-04-05
\| * \| \|	Fix #7124: Warning "Ignoring implicit status" does not provide line number	Maxime Dénès	2018-04-05
\|/ / /
* \| \|	Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.	Hugo Herbelin	2018-04-04
\|\ \ \
\| * \| \|	Fix #6257: anomaly with Printing Projections and Context.	Gaëtan Gilbert	2018-03-30