coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	universes_of_constr don't include universes of monomorphic constants	Gaëtan Gilbert	2018-06-26
\| \| \| \| \|	Apparently it was not useful. I don't remember what I was thinking when I added it.
*	[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.
*	Remove some occurrences of Evd.empty	Maxime Dénès	2018-05-25
\| \| \| \|	We address the easy ones, but they should probably be all removed.
*	[vernac] taint two out-of-api `to_constr` use in `comDefinition`.	Emilio Jesus Gallego Arias	2018-05-07
\| \| \| \|	This should fix #7448 and #7265.
*	[econstr] Forbid calling `to_constr` in open terms.	Emilio Jesus Gallego Arias	2018-03-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We forbid calling `EConstr.to_constr` on terms that are not evar-free, as to progress towards enforcing the invariant that `Constr.t` is evar-free. [c.f. #6308] Due to compatibility constraints we provide an optional parameter to `to_constr`, `abort` which can be used to overcome this restriction until we fix all parts of the code. Now, grepping for `~abort:false` should return the questionable parts of the system. Not a lot of places had to be fixed, some comments: - problems with the interface due to `Evd/Constr` [`Evd.define` being the prime example] do seem real! - inductives also look bad with regards to `Constr/EConstr`. - code in plugins needs work. A notable user of this "feature" is `Obligations/Program` that seem to like to generate kernel-level entries with free evars, then to scan them and workaround this problem by generating constants.
*	Rename some universe minimizing "normalize" functions to "minimize"	Gaëtan Gilbert	2018-03-06
\| \| \| \|	UState normalize -> minimize, Evd nf_constraints -> minimize_universes
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	Merge code paths in interp_definition and cleanup a bit.	Gaëtan Gilbert	2017-12-21
\|
*	[vernac] Cleanup of do_definition.	Emilio Jesus Gallego Arias	2017-12-18
\| \| \| \| \|	We remove a few old-style normalization and try to use the newer APIs, however, it is hard to say whether the right magic is being used.
*	[flags] Make program_mode a parameter for commands in vernac.	Emilio Jesus Gallego Arias	2017-12-17
\| \| \| \|	This is useful as it allows to reflect program_mode behavior as an attribute.
*	[vernac] Split `command.ml` into separate files.	Emilio Jesus Gallego Arias	2017-12-17
	Over the time, `Command` grew organically and it has become now one of the most complex files in the codebase; however, its functionality is well separated into 4 key components that have little to do with each other. We thus split the file, and also document the interfaces. Some parts of `Command` export tricky internals to use by other plugins, and it is common that plugin writers tend to get confused, so we are more explicit about these parts now. This patch depends on #6413.