aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
Commit message (Collapse)AuthorAge
* Evarutil.(e_)new_Type: remove unused env argumentGravatar Gaëtan Gilbert2018-07-03
|
* Remove unused function Evd.whd_sort_variableGravatar Gaëtan Gilbert2018-07-03
|
* Remove unused output of Universes.normalize_univ_variablesGravatar Gaëtan Gilbert2018-07-03
|
* Remove unused env argument to fresh_sort_in_familyGravatar Gaëtan Gilbert2018-07-03
| | | | (Universes and Evd)
* Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
| | | | | | | | | This shall eventually allow to use contexts of declarations in the definition of the "Case" constructor. Basically, this means that Constr now includes Context and that the "t" types of Context which were specialized on constr are not defined in Constr (unfortunately using a heavy boilerplate).
* Merge PR #7863: Remove Sorts.contentsGravatar Pierre-Marie Pédrot2018-06-27
|\
* \ Merge PR #7826: evd: restrict_evar with candidates, can raise NoCandidatesLeftGravatar Hugo Herbelin2018-06-26
|\ \
* \ \ Merge PR #7906: universes_of_constr don't include universes of monomorphic ↵Gravatar Pierre-Marie Pédrot2018-06-26
|\ \ \ | | | | | | | | | | | | constants
| | | * Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
| |_|/ |/| |
| * | universes_of_constr don't include universes of monomorphic constantsGravatar Gaëtan Gilbert2018-06-26
| | | | | | | | | | | | | | | Apparently it was not useful. I don't remember what I was thinking when I added it.
* | | Merge PR #7827: [engine] safe [add_unification_pb] interfaceGravatar Pierre-Marie Pédrot2018-06-23
|\ \ \ | |/ / |/| |
* | | Merge PR #7797: Remove reference name type.Gravatar Enrico Tassi2018-06-19
|\ \ \
* | | | Fix #7421: constr_eq ignores universe constraints.Gravatar Gaëtan Gilbert2018-06-18
| | | | | | | | | | | | | | | | | | | | The test isn't quite the one in #7421 because that use of algebraic universes is wrong.
| * | | Remove reference name type.Gravatar Maxime Dénès2018-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.
| | * evd: restrict_evar with candidates, can raise NoCandidatesLeftGravatar Matthieu Sozeau2018-06-15
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When restricting an evar with candidates, raise an exception if this restriction would leave the evar without candidates, i.e. unsolvable. - evarutil: mark restricted evars as "cleared" They would otherwise escape being catched by the [advance] function of clenv, and result in dangling evars not being registered to the shelf. - engine: restrict_evar marks it cleared, update the future goals We make the new evar a future goal and remove the old one. If we did nothing, [unshelve tac] would work correctly as it uses [Proofview.advance] to find the shelved goals, going through the cleared evar. But [Unshelve] would fail as it expects only undefined evars on the shelf and throws away the defined ones.
| * evd/evarutil: safe [add_unification_pb] interface, taking EConstr'sGravatar Matthieu Sozeau2018-06-15
|/ | | | Avoid adding the same unification problem twice, module evar instantiation.
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | | | - move_location to proofs/logic. - intro_pattern_naming to Namegen.
* [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.