aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
Commit message (Collapse)AuthorAge
* Merge PR #6675: [proofview] enter_one: add __LOC__ argument to get relevant ↵Gravatar Maxime Dénès2018-02-01
|\ | | | | | | error msg
| * Proofview: enter_one: add __LOC__ argument to get relevant error msgGravatar Enrico Tassi2018-01-31
| | | | | | | | | | | | | | | | | | | | | | | | | | The type discipline of the tactic monad does not distinguish between mono-goal and multi-goal tactics. Unfortunately enter_one "asserts false" if called on 0 or > 1 goals. The __LOC__:string argument can be used to make the error message more helpful (since the backtrace is pointless inside the monad). The intended usage is "Goal.enter_one ~__LOC__ (fun gl -> ..". The __LOC__ variable is filled in by the OCaml compiler with the current file name and line number.
* | Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Gravatar Maxime Dénès2018-01-31
|\ \
* \ \ Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.Gravatar Maxime Dénès2018-01-22
|\ \ \ | |_|/ |/| |
| * | Define EConstr version of [push_rec_types].Gravatar Cyprien Mangin2018-01-19
| | |
* | | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Maxime Dénès2018-01-18
|\ \ \ | |/ / |/| |
* | | Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)Gravatar Maxime Dénès2018-01-17
|\ \ \
| | * | Add a test that `prod_applist_assum` reduces the right number of let-insGravatar Jasper Hugunin2018-01-17
| | | |
| | * | Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Jasper Hugunin2018-01-17
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fixes #6490. `prod_applist_assum` is copied from `kernel/term.ml` to `engine/termops.ml`, and adjusted to work with econstr. This change uncovered a bug in `Hipattern.match_with_nodep_ind`, where `has_nodep_prod_after` counts both products and let-ins, but was only being passed `mib.mind_nparams`, which does not count let-ins. Replaced with (Context.Rel.length mib.mind_params_ctxt).
| | * Use a more efficient substitution composition in evar hypothesis naming.Gravatar Pierre-Marie Pédrot2018-01-04
| | |
| | * Cleanup name-binding structure for fresh evar name generation.Gravatar Pierre-Marie Pédrot2018-01-02
| | | | | | | | | | | | | | | | | | | | | We simply use a record and pack the rel and var substitutions in it. We also properly compose variable substitutions. Fixes #6534: Fresh variable generation in case of clash is buggy.
* | | Moving some universe substitution code out of the kernel.Gravatar Pierre-Marie Pédrot2017-12-30
| |/ |/| | | | | | | | | This code was not used at all inside the kernel, it was related to universe unification that happens in the upper layer. It makes more sense to put it somewhere upper.
* | Merge PR #6222: Share computation of unifiable evarsGravatar Maxime Dénès2017-12-22
|\ \
* \ \ Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Gravatar Maxime Dénès2017-12-18
|\ \ \
* \ \ \ Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`Gravatar Maxime Dénès2017-12-15
|\ \ \ \
* \ \ \ \ Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\ \ \ \ \
| | | * | | [econstr] Add a couple of new API functions.Gravatar Emilio Jesus Gallego Arias2017-12-13
| | |/ / / | | | | | | | | | | | | | | | These are also convenient from `vernac` [to be used in future PRs].
| | * / / [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 #6368: [api] Remove yet another type alias.Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \
| | * | | | | [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
| |/ / / / / |/| | | | |
| | | * | | [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
| | * | | [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.
* | | | Merge PR #6290: Rename update to set, Fixes #6196Gravatar Maxime Dénès2017-12-07
|\ \ \ \
| | * | | 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].
| * | | Rename update to set, fixes #6196Gravatar Paul Steckler2017-12-05
| | | |
| | | * Fix #6297: handle constraints like (u+1 <= Set/Prop)Gravatar Gaëtan Gilbert2017-12-01
| | |/ | |/|
* | | 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.
* | | Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
|/ / | | | | | | | | | | | | | | They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced
* | 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
|\ \ \
| * | | [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.
| | * | Forbid repeated names in universe binders.Gravatar Gaëtan Gilbert2017-11-25
| | | |
| | * | 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
| | | |
| | * | Make restrict_universe_context stronger.Gravatar Gaëtan Gilbert2017-11-25
| | | | | | | | | | | | | | | | | | | | | | | | This fixes BZ#5717. Also add a test and fix a changed test.
* | | | [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.
| * | restrict_universe_context: do not prune named universes.Gravatar Gaëtan Gilbert2017-11-24
| | |
| * | Stop exposing UState.universe_context and its Evd wrapper.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | | | | | | | We can enforce properties through check_univ_decl, or get an arbitrary ordered context with UState.context / Evd.to_universe_context (the later being a new wrapper of the former).
| * | Separate checking univ_decls and obtaining universe binder names.Gravatar Gaëtan Gilbert2017-11-24
| | |
| * | Use Maps and ids for universe bindersGravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | Before sometimes there were lists and strings.
| * | Use type Universes.universe_binders.Gravatar Gaëtan Gilbert2017-11-24
|/ /
* | Merge PR #6203: Fix universe polymorphic Program obligations.Gravatar Maxime Dénès2017-11-23
|\ \
* | | [api] A few more minor deprecation notices.Gravatar Emilio Jesus Gallego Arias2017-11-22
| | | | | | | | | | | | Note the problem with `create_evar_defs`.
* | | [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
| | | | | | | | | | | | | | | | | | | | | We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`.
| * | Fix universe polymorphic Program obligations.Gravatar Matthieu Sozeau2017-11-22
| | | | | | | | | | | | | | | | | | The universes of the obligations should all be non-algebraic as they might appear in instances of other obligations and instances only take non-algebraic universes as arguments.
* | | [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
| | | | | | | | | | | | | | | | | | We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization.
| | * Experimenting with a fine-grained cache for undefined evars in evinfos.Gravatar Pierre-Marie Pédrot2017-11-21
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-22 07:41:37 +0000