aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/comDefinition.ml
Commit message (Collapse)AuthorAge
* [api] Move `Constrexpr` to the `interp` module.Gravatar Emilio Jesus Gallego Arias2018-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.emptyGravatar Maxime Dénès2018-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`.Gravatar Emilio Jesus Gallego Arias2018-05-07
| | | | This should fix #7448 and #7265.
* [econstr] Forbid calling `to_constr` in open terms.Gravatar Emilio Jesus Gallego Arias2018-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"Gravatar Gaëtan Gilbert2018-03-06
| | | | UState normalize -> minimize, Evd nf_constraints -> minimize_universes
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Merge code paths in interp_definition and cleanup a bit.Gravatar Gaëtan Gilbert2017-12-21
|
* [vernac] Cleanup of do_definition.Gravatar Emilio Jesus Gallego Arias2017-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.Gravatar Emilio Jesus Gallego Arias2017-12-17
| | | | This is useful as it allows to reflect program_mode behavior as an attribute.
* [vernac] Split `command.ml` into separate files.Gravatar Emilio Jesus Gallego Arias2017-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.