| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
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).
|
|
|
|
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.
|
|
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.
|
|
|
|
|
|
|
|
|
|
These are also convenient from `vernac` [to be used in future PRs].
|
|
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.
|
|
|
|
|
|
|
|
|
|
New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
|
|
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.
|
|
|
|
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].
|
|
|
|
|
|
- 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.
|
|
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
|
|
|
|
|
|
There don't really bring anything, we also correct some minor nits
with the printing function.
|
|
|
|
|
|
|
|
This fixes BZ#5717.
Also add a test and fix a changed test.
|
|
We also remove some internal implementation details from the mli file,
there due historical reasons.
|
|
This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.
|
|
|
|
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).
|
|
|
|
Before sometimes there were lists and strings.
|
|
|
|
|
|
Note the problem with `create_evar_defs`.
|
|
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`.
|
|
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.
|
|
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.
|
|
|
|
It is actually polynomial with a big exponent, probably quartic. This was due
to the Proofview.unifiable algorithm that kept recomputing the free evars of
an evar info. We share the computation instead.
This does not make the contrived example compile in a reasonable amount of time,
but it does make smaller instances compile way quicker than before. Indeed, the
example is essentially quadratic in size as all evars refer to the previously
defined ones in their signature.
|
|
I followed what seems to be the intention of the code, with the
original intention of remove the global imperative proof state.
However, I fully fail to see why the new API is better than the old
one. In fact the opposite seems the contrary.
Still big parts of the "new proof engine" seem unfinished, and I'm
afraid I am not the right person to know what direction things should
take.
|
