coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\| \| * \|	Fixes #7110 ("as" untested while looking for notation for nested patterns).	Hugo Herbelin	2018-03-29
\| \|/ /
* / /	Patterns: Accepting patterns in PFix and PCofix and not only constr.	Hugo Herbelin	2018-03-28
\|/ /
\| *	[api] Deprecate a couple of aliases that we missed.	Emilio Jesus Gallego Arias	2018-03-28
\|/
*	[located] Push inner locations in `reference` to a CAst.t node.	Emilio Jesus Gallego Arias	2018-03-09
*	[located] More work towards using CAst.t	Emilio Jesus Gallego Arias	2018-03-09
*	Revert "Merge PR #873: New strategy based on open scopes for deciding which n...	Maxime Dénès	2018-03-09