aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
Commit message (Collapse)AuthorAge
* Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
| | | | | | | | | | | | Virtually all classifications of vernacular commands (the STM classifier, "filtered commands", "navigation commands", etc.) were broken in presence of control vernaculars like Time, Timeout, Fail. Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac Debug in CoqIDE. This change introduces a type separation between vernacular controls and vernacular commands, together with an "under_control" combinator.
* Merge PR #6419: [vernac] Split `command.ml` into separate files.Gravatar Maxime Dénès2017-12-18
|\
* \ Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Gravatar Maxime Dénès2017-12-18
|\ \
| | * [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.
* | Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`Gravatar Maxime Dénès2017-12-15
|\ \
| | * [econstr] Switch constrintern API to non-imperative style.Gravatar Emilio Jesus Gallego Arias2017-12-15
| | | | | | | | | | | | | | | We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step desirable to progress with EConstr there.
* | | Merge PR #6341: Fix anomaly in [Type foo] command, + print uctx like Check.Gravatar Maxime Dénès2017-12-13
|\ \ \
* \ \ \ Merge PR #6251: [proof] Embed evar_map in RefinerError exception.Gravatar Maxime Dénès2017-12-13
|\ \ \ \
| | | | * [econstr] Small cleanup in `vernac/lemmas`Gravatar Emilio Jesus Gallego Arias2017-12-13
| | | |/
| | | * [econstr] Cleanup in `vernac/classes.ml`.Gravatar Emilio Jesus Gallego Arias2017-12-13
| |_|/ |/| | | | | | | | | | | | | | | | | | | | We fix quite a few types, and perform some cleanup wrt to the evar_map, in particular we prefer to thread it now as otherwise it may become trickier to check when we are using the correct one. Thanks to @SkySkimmer for lots of comments and bug-finding.
* | | Merge PR #6275: [summary] Allow typed projections from global state.Gravatar Maxime Dénès2017-12-12
|\ \ \
* \ \ \ Merge PR #6270: [toplevel] Properly redirect stdout on `Redirect` vernac.Gravatar Maxime Dénès2017-12-11
|\ \ \ \
| | | | * Fix anomaly in [Type foo] command, + print uctx like Check.Gravatar Gaëtan Gilbert2017-12-11
| | | | |
| | | * | [proof] Embed evar_map in RefinerError exception.Gravatar Emilio Jesus Gallego Arias2017-12-11
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The exception needs to carry aroud a pair of `env, sigma` so printing is correct. This gets rid of a few global calls, and it is IMO the right thing to do. While we are at it, we incorporate some fixes to a couple of additional printing functions missing the `env, sigma` pair.
* | | | Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Gravatar Maxime Dénès2017-12-11
|\ \ \ \
* | | | | [api] Remove kernel dependency on intf (Decl_kind)Gravatar Emilio Jesus Gallego Arias2017-12-10
| |_|_|/ |/| | | | | | | | | | | | | | | | | | | We more the `recursivity_kind` type to `Declarations`, this indeed makes sense, and now `Decl_kind` morally lives in `library` as it should.
| | | * [summary] Adapt STM to the new Summary API.Gravatar Emilio Jesus Gallego Arias2017-12-09
| | | | | | | | | | | | | | | | | | | | | | | | We need to a partial restore. I think that we could design a better API, but further work on the toplevel state should improve it progressively.
| | | * [summary] Allow typed projections from global state + rework of internals.Gravatar Emilio Jesus Gallego Arias2017-12-09
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In the transition towards a less global state handling we have the necessity of mix imperative setting [notably for the modules/section code] and functional handling of state [notably in the STM]. In that scenario, it is very convenient to have typed access to the Coq's `summary`. Thus, I reify the API to support typed access to the `summary`, and implement such access in a couple of convenient places. We also update some internal datatypes to simplify the `frozen` data type. We also remove the use of hashes as it doesn't really make things faster, and most operations are now over `Maps` anyways. I believe this goes in line with recent work by @ppedrot. We also deprecate the non-typed accessors, which were only supposed to be used in the STM, which is now ported to the finer primitives.
| * | Fix #6323: stronger restrict universe context vs abstract.Gravatar Gaëtan Gilbert2017-12-06
|/ / | | | | | | | | | | | | | | In the test we do [let X : Type@{i} := Set in ...] with Set abstracted. The constraint [Set < i] was lost in the abstract. Universes of a monomorphic reference [c] are considered to appear in the term [c].
* | Merge PR #890: Global universe declarationsGravatar Maxime Dénès2017-12-05
|\ \
* | | [vernac] Couple of tweaks missing from previous PRs.Gravatar Emilio Jesus Gallego Arias2017-12-04
| | | | | | | | | | | | | | | In particular we must invalidate the state cache in the case of an exception.
| * | Cleanup API for registering universe binders.Gravatar Matthieu Sozeau2017-12-01
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Regularly declared for for polymorphic constants - Declared globally for monomorphic constants. E.g mono@{i} := Type@{i} is printed as mono@{mono.i} := Type@{mono.i}. There can be a name clash if there's a module and a constant of the same name. It is detected and is an error if the constant is first but is not detected and the name for the constant not registered (??) if the constant comes second. Accept VarRef when registering universe binders Fix two problems found by Gaëtan where binders were not registered properly Simplify API substantially by not passing around a substructure of an already carrier-around structure in interpretation/declaration code of constants and proofs Fix an issue of the stronger restrict universe context + no evd leak This is uncovered by not having an evd leak in interp_definition, and the stronger restrict_universe_context. This patch could be backported to 8.7, it could also be triggered by the previous restrict_context I think.
* | Merge PR #6233: [proof] [api] Rename proof types in preparation for ↵Gravatar Maxime Dénès2017-12-01
|\ \ | | | | | | | | | functionalization.
* \ \ Merge PR #1049: Remove obsolete localityGravatar Maxime Dénès2017-11-30
|\ \ \
* \ \ \ Merge PR #6244: [lib] [api] Introduce record for `object_prefix`Gravatar Maxime Dénès2017-11-30
|\ \ \ \
* \ \ \ \ Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as ↵Gravatar Maxime Dénès2017-11-30
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | instance.
| | | * | | Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We remove deprecated syntax "Coercion Local" and such, and seize the opportunity to refactor some code around vernac_expr. We also do a small fix on the STM classification, which didn't know about Let Fixpoint and Let CoFixpoint. This is a preliminary step for the work on attributes.
| | * | | [lib] [api] Introduce record for `object_prefix`Gravatar Emilio Jesus Gallego Arias2017-11-29
| | | | | | | | | | | | | | | | | | | | | | | | | This is a minor cleanup adding a record in a try to structure the state living in `Lib`.
| | | * | [proof] [api] Rename proof types in preparation for functionalization.Gravatar Emilio Jesus Gallego Arias2017-11-29
| |_|/ / |/| | | | | | | | | | | | | | | In particular `Proof_global.t` will become a first class object for the upper parts of the system in a next commit.
* | | | Merge PR #6199: [vernac] Uniformize type of vernac interpretation.Gravatar Maxime Dénès2017-11-29
|\ \ \ \
| | | | * [toplevel] Properly redirect stdout on `Redirect` vernac.Gravatar Emilio Jesus Gallego Arias2017-11-28
| |_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | Fixes #6130, it was a silly omission from a previous output refactoring. We redirect all channels as this was the implied semantics of the old command.
| | * | Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gravatar Gaëtan Gilbert2017-11-28
| |/ / |/| |
* | | Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\ \ \
* \ \ \ Merge PR #6248: [api] Remove aliases of `Evar.t`Gravatar Maxime Dénès2017-11-28
|\ \ \ \ | |_|_|/ |/| | |
| | | * [vernac] Adjust `interp` to pass polymorphic in the attributes.Gravatar Emilio Jesus Gallego Arias2017-11-27
| | | |
| | | * [vernac] Add polymorphic to the type of vernac interpration options.Gravatar Emilio Jesus Gallego Arias2017-11-27
| | | |
| | | * [vernac] Start to uniformize type of vernac interpretation.Gravatar Emilio Jesus Gallego Arias2017-11-27
| |_|/ |/| | | | | | | | | | | | | | | | | | | | In particular, we put all the context in the atts structure, and generalize the type of the parameters of a vernac. I hope this helps people working on "attributes", my motivation is indeed having a more robust interpretation.
* | | Merge PR #6241: [lib] Generalize Control.timeout type.Gravatar Maxime Dénès2017-11-27
|\ \ \
* \ \ \ Merge PR #6041: Protecting the printing of filenames with spaceGravatar Maxime Dénès2017-11-27
|\ \ \ \
| | | * | [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
| |_|/ / |/| | | | | | | | | | | | | | | There don't really bring anything, we also correct some minor nits with the printing function.
| | | * Restrict universe context when declaring constants in obligations.Gravatar Gaëtan Gilbert2017-11-25
| | | |
| | | * Fix #5347: unify declaration of axioms with and without bound univs.Gravatar Gaëtan Gilbert2017-11-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note that this makes the following syntax valid: Axiom foo@{i} bar : Type@{i}. (ie putting a universe declaration on the first axiom in the list, the declaration then holds for the whole list).
| | | * Universe binders survive sections, modules and compilation.Gravatar Gaëtan Gilbert2017-11-25
| | | |
| | | * Allow local universe renaming in Print.Gravatar Gaëtan Gilbert2017-11-25
| | | |
| | | * Fix obligations handling of universes anticipating stronger restrictGravatar Matthieu Sozeau2017-11-25
| | | |
| | * | [lib] Generalize Control.timeout type.Gravatar Emilio Jesus Gallego Arias2017-11-24
| |/ / |/| | | | | | | | | | | We also remove some internal implementation details from the mli file, there due historical reasons.
| | * Use Entries.constant_universes_entry more.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | | | | | | | This reduces conversions between ContextSet/UContext and encodes whether we are polymorphic by which constructor we use rather than using some boolean.
| | * When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | | | | | | | | | | | | | Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved.
| | * Fix defining non primitive projections with abstracted universes.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | | | | I think this only affects printing (in the new test you would get [Var (0)] when printing runwrap) but is still ugly.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 18:49:32 +0000