aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
Commit message (Collapse)AuthorAge
* [api] Misctypes removal: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
|
* Add a bit of doc to EConstr.decompose_lam*Gravatar Gaëtan Gilbert2018-06-08
|
* Merge PR #7706: Fix wrong deprecation msgGravatar Pierre-Marie Pédrot2018-06-07
|\
* \ Merge PR #6874: [econstr] Some minor tweaksGravatar Pierre-Marie Pédrot2018-06-07
|\ \
| | * Update evarutil.mliGravatar Matthieu Sozeau2018-06-05
| | | | | | | | | Actually all the new_ functions are in evarutil still
| | * Fix wrong deprecation msgGravatar Matthieu Sozeau2018-06-05
| |/ |/|
* | Merge PR #7495: Fix restrict_universe_contextGravatar Matthieu Sozeau2018-06-05
|\ \
| | * [econstr] Remove some Unsafe.to_constr use.Gravatar Emilio Jesus Gallego Arias2018-06-04
| | | | | | | | | | | | Most of it seems straightforward.
| | * [termops] Update type of function, anyways not used in the codebase.Gravatar Emilio Jesus Gallego Arias2018-06-04
| |/ |/| | | | | Note that `Assumptions` ships its own copy, but for `Constr.t`.
* | Merge PR #7216: Replace uses of Termops.dependent by more specific functions.Gravatar Matthieu Sozeau2018-06-04
|\ \
* | | [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.
* | | [api] Remove deprecated objects in engine / interp / libraryGravatar Emilio Jesus Gallego Arias2018-05-30
| | |
* | | [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We remove most of what was deprecated in `Term`. Now, `intf` and `kernel` are almost deprecation-free, tho I am not very convinced about the whole `Term -> Constr` renaming but I'm afraid there is no way back. Inconsistencies with the constructor policy (see #6440) remain along the code-base and I'm afraid I don't see a plan to reconcile them. The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a good idea as someone added a `List` module inside it.
| | * Fix restrict_universe_contextGravatar Gaëtan Gilbert2018-05-30
| |/ |/|
* | Merge PR #7521: Fix soundness bug with VM/native and cofixpointsGravatar Pierre-Marie Pédrot2018-05-28
|\ \
| * | Unify pre_env and envGravatar Maxime Dénès2018-05-28
| | | | | | | | | | | | | | | We now have only two notions of environments in the kernel: env and safe_env.
* | | Remove some occurrences of Evd.emptyGravatar Maxime Dénès2018-05-25
|/ / | | | | | | We address the easy ones, but they should probably be all removed.
* | Collecting Map.smart_* functions into a module Map.Smart.Gravatar Hugo Herbelin2018-05-23
| |
* | Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.Gravatar Hugo Herbelin2018-05-23
| |
* | Collecting Array.smart_* functions into a module Array.Smart.Gravatar Hugo Herbelin2018-05-23
| |
* | Split off Universes functions for minimization.Gravatar Gaëtan Gilbert2018-05-17
| | | | | | | | This finishes the splitting of Universes.
* | Make Universes.refresh_constraints internal to UStateGravatar Gaëtan Gilbert2018-05-17
| |
* | Split off Universes functions about substitutions and constraintsGravatar Gaëtan Gilbert2018-05-17
| |
* | Move solve_constraint_system near its only use site (comInductive)Gravatar Gaëtan Gilbert2018-05-17
| |
* | Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
| |
* | Split off Universes functions dealing with names.Gravatar Gaëtan Gilbert2018-05-17
| | | | | | | | This API is a bit strange, I expect it will change at some point.
* | Make set minimization option internal to UniversesGravatar Gaëtan Gilbert2018-05-17
| |
* | Merge PR #7359: Reduce usage of evar_map referencesGravatar Pierre-Marie Pédrot2018-05-17
|\ \
| * | Use evd_combX in Cases.Gravatar Gaëtan Gilbert2018-05-14
| | |
| * | Convert clear_hyps_in_evi to state passing style.Gravatar Gaëtan Gilbert2018-05-11
| | |
| * | Deprecate most evarutil evdref functionsGravatar Gaëtan Gilbert2018-05-11
| | | | | | | | | | | | clear_hyps remain with no alternative
* | | Don't use ref universe_opt_substGravatar Gaëtan Gilbert2018-05-08
|/ /
* | [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
| | | | | | | | | | | | | | | | | | | | | | | | | | In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at.
* | Merge PR #7375: Implement to_constr with nf_evars_and_universes_opt_substGravatar Pierre-Marie Pédrot2018-05-03
|\ \
* \ \ Merge PR #6935: Separate universe minimization and evar normalization functionsGravatar Pierre-Marie Pédrot2018-04-30
|\ \ \
| | * | Implement to_constr with nf_evars_and_universes_opt_substGravatar Gaëtan Gilbert2018-04-29
| | | |
| | * | Fix nf_evars_universes_opt_subst: recurse on univs, nf undef evarsGravatar Gaëtan Gilbert2018-04-28
| |/ / |/| |
* | | Merge PR #6892: Cleanup implementation of normalize_context_set a bitGravatar Pierre-Marie Pédrot2018-04-28
|\ \ \
* \ \ \ Merge PR #6866: Slight improvement of messages related to direct and ↵Gravatar Pierre-Marie Pédrot2018-04-25
|\ \ \ \ | | | | | | | | | | | | | | | indirect uses of tactic `clear`.
* \ \ \ \ Merge PR #307: Adding a flag to support different naming modes for evar ↵Gravatar Pierre-Marie Pédrot2018-04-24
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | hypotheses.
| | * | | | Improving error message for clear tactic (and indirect uses of it).Gravatar Hugo Herbelin2018-04-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Be more precise when trying to clear an hypothesis which occurs implicitly in a global constant. - Warns if destruct/induction cannot clear an hypothesis occurring implicitly in a global. In the first case, the change in situation Section A. Variable a:nat. Definition b:=a=a. Goal b=b. clear a. is: - before: "a is used in conclusion" - after: "a is used implicitly in b in conclusion" In the second case: Section A. Variable a:nat. Definition b:=a=a. Goal b=b. destruct a. produces a warning: "Cannot remove a, it is used implicitly in b".
| * | | | | Adding a flag to support different naming modes for evar hypotheses.Gravatar Hugo Herbelin2018-04-24
| |/ / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Four modes currently supported to deal with clashes: 1. Failing in case of clash 2. Renaming the most recent one 3. Renaming the previous hypothesis of same name if not a section variable 4. Renaming the previous hypothesis of same name even if a section variable The current mode is 3. Keeping it active by default
* / / / / [api] Relocate `intf` modules according to dependency-order.Gravatar Emilio Jesus Gallego Arias2018-04-23
|/ / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In a component-based source code organization of Coq `intf` doesn't fit very well, as it sits in bit of "limbo" between different components, and indeed, encourages developers to place types in sometimes random places wrt the hierarchy. For example, lower parts of the system reference `Vernacexpr`, which morally lives in a pretty higher part of the system. We move all the files in `intf` to the lowest place their dependencies can accommodate: - `Misctypes`: is used by Declaremod, thus it has to go in `library` or below. Ideally, this file would disappear. - `Evar_kinds`: it is used by files in `engine`, so that seems its proper placement. - `Decl_kinds`: used in `library`, seems like the right place. [could also be merged. - `Glob_term`: belongs to pretyping, where it is placed. - `Locus`: ditto. - `Pattern`: ditto. - `Genredexpr`: depended by a few modules in `pretyping`, seems like the righ place. - `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and could be fixed, as this module should be declared in `interp` which is the one eliminating it. - `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed as it contains stuff it shouldn't. The right place should be `parsing`. - `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`. - `Notation_term`: First place used is `interp`, seems like the right place. Additionally, for some files it could be worth to merge files of the form `Foo` with `Foo_ops` in the medium term, as to create proper ADT modules as done in the kernel with `Name`, etc...
| | * / Deprecate mixing univ minimization and evm normalization functions.Gravatar Gaëtan Gilbert2018-04-17
| |/ / |/| | | | | | | | Normalization sounds like it should be semantically noop.
| * | univ minimization: comment [enforce_uppers]Gravatar Gaëtan Gilbert2018-04-13
| | |
| * | univ minimization [enforce_upper]: replace Option.get with matchGravatar Gaëtan Gilbert2018-04-13
| | |
| * | univ minimization: Partially let-lift [enforce_uppers]Gravatar Gaëtan Gilbert2018-04-13
| | |
| * | univ minimization: rename acc' -> enforce_uppersGravatar Gaëtan Gilbert2018-04-13
| | |
| * | univ minimization: use shadowing moreGravatar Gaëtan Gilbert2018-04-13
| | | | | | | | | | | | | | | This avoids having multiple highly similar things in scope when we only want one of them.
| * | univ minimization: let-lift [not_lower]Gravatar Gaëtan Gilbert2018-04-13
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 18:29:01 +0000