coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Remove reference name type.	Maxime Dénès	2018-06-18
\| \| \| \| \| \| \| \|	reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
*	[api] Remove Misctypes.	Emilio Jesus Gallego Arias	2018-06-12
\| \| \| \|	We move the last 3 types to more adequate places.
*	[api] Misctypes removal: miscellaneous aliases.	Emilio Jesus Gallego Arias	2018-06-12
\|
*	[api] Move `Constrexpr` to the `interp` module.	Emilio Jesus Gallego Arias	2018-05-31
	Continuing the interface cleanup we place `Constrexpr` in the internalization module, which is the one that eliminates it. This slims down `pretyping` considerably, including removing the `Univdecls` module which existed only due to bad dependency ordering in the first place. Thanks to @ Skyskimmer we also remove a duplicate `univ_decl` definition among `Misctypes` and `UState`. This is mostly a proof of concept yet as it depends on quite a few patches of the tree. For sure some tweaks will be necessary, but it should be good for review now. IMO the tree is now in a state where we can could easy eliminate more than 10 modules without any impact, IMHO this is a net saving API-wise and would help people to understand the structure of the code better.