| Age | Commit message (Collapse) | Author |
|---|
|
cleanup of constrintern.ml
Reviewed-by: SkySkimmer
Ack-by: ppedrot
|
|
|
|
Namely, WrongNumargInductive and WrongNumargConstructor.
|
|
We also simplify the whole process of interpretation of cases pattern
on the way.
|
|
|
|
constants/inductives/constructors
Reviewed-by: SkySkimmer
|
|
Reviewed-by: mattam82
|
|
|
|
This allows proper treatment in notations, ie fixes #13303
The "glob" representation of universes (what pretyping sees) contains
only fully interpreted (kernel) universes and unbound universe
ids (for non Strict Universe Declaration).
This means universes need to be understood at intern time, so intern
now has a new "universe binders" argument. We cannot avoid this due to
the following example:
~~~coq
Module Import M. Universe i. End M.
Definition foo@{i} := Type@{i}.
~~~
When interning `Type@{i}` we need to know that `i` is locally bound to
avoid interning it as `M.i`.
Extern has a symmetrical problem:
~~~coq
Module Import M. Universe i. End M.
Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
Print foo. (* must not print Type@{i} -> Type@{i} *)
~~~
(Polymorphic as otherwise the local `i` will be called `foo.i`)
Therefore extern also takes a universe binders argument.
Note that the current implementation actually replaces local universes
with names at detype type. (Asymmetrical to pretyping which only gets
names in glob terms for dynamically declared univs, although it's
capable of understanding bound univs too)
As such extern only really needs the domain of the universe
binders (ie the set of bound universe ids), we just arbitrarily pass
the whole universe binders to avoid putting `Id.Map.domain` at every
entry point.
Note that if we want to change so that detyping does not name locally
bound univs we would need to pass the reverse universe binders (map
from levels to ids, contained in the ustate ie in the evar map) to
extern.
|
|
|
|
To tie the knot (since the evar depends on the evar type and the
source of the evar type of the evar), we use an "update_source"
function.
An alternative could be to provide a function to build both an evar
with its evar type directly in evd.ml...
|
|
erroneously caught
Reviewed-by: ppedrot
|
|
Fixes #7430 and fixes #10968
This commit makes the following changes:
- Add an exception `Signal` used to convert OCaml signals to exceptions.
`Signal` is registered as critical in `CErrors` to avoid being caught in the
wrong `with` clauses.
- Make `Control.timeout` into a safer interface based on `option` instead of
exceptions.
- Modify `tclTIMEOUT` to fail with `CErrors.Timeout` instead of
`Logic_monad.Tac_timeout`, as was already advertised in the ocamldoc documentation.
- Removes `Logic_monad.Tac_timeout` altogether because it no longer has a use.
|
|
primitive projection was wrongly supposed to be already inferred
Reviewed-by: gares
|
|
template poly
Reviewed-by: gares
Reviewed-by: herbelin
|
|
This is to make more explicit that arguments of the projection are not
kept.
We seize this opportunity to use QGlobRef equality on GlobRef.
|
|
type.
This was a case where expand_projections was calling find_mrectype
which was expecting the argument of the projection to be an inductive.
We could have ensured that this type is at least the appropriate
inductive applied to fresh evars, but this expand_projections was in
practice used for checking the applicability of canonical structures
and the unifiability of the parameters of the projections is anyway a
consequence of the unifiability of the principal argument of the
projections. So, the latter is enough.
|
|
locating fix
Reviewed-by: gares
|
|
Reviewed-by: gares
|
|
of the definition of the metas
Reviewed-by: mattam82
|
|
of unification
Reviewed-by: mattam82
|
|
|
|
We ensure that when imitation stops to be possible, we postpone an
equation of the type of the subterm (and not of the arbitrary type of
an evar possibly depending on this subterm).
|
|
It remains to accept resolving Type(u)<=Prop for u arbitrary sort variable.
|
|
See 742ef62fe8050a6865d06bd644e30cbec0e7eb02
Fix #13366
Fix #9809
|
|
sort elimination constraints
Reviewed-by: gares
|
|
(solve_simple_eqn).
The bug was that an assumption could be interpreted as a local
definition and wrongly expanded.
It triggered rarely because it involved mixing let-ins and
local assumptions + imitation under binders.
|
|
Even though it is not strongly supposed to be raised.
|
|
handler in NotFoundInstance
Reviewed-by: ejgallego
|
|
Fixes #13266 (see #12675, 8641cb7385).
|
|
In Evar := C[Meta] problems of unification.ml, and C[ ] contains
binders, Meta was wrongly considered by pose_all_metas_as_evars as
under these binders (while Metas are always defined in the initial
context of the unification problem).
|
|
Fix #13354
This change is very specific to array, but should not be a significant
obstacle to generalization of the feature to eg axioms if we want to later.
|
|
naming
Ack-by: gares
Reviewed-by: ppedrot
|
|
Instead we store that data in the native code that was generated in adapt
the compilation scheme accordingly. Less indirections and less imperative
tinkering makes the code safer.
The global symbol table was originally introduced in #10359 as a way not to
depend on the Global module in the generated code. By storing all the
native-related information in the cmxs file itself, this PR also makes other
changes easier, such as e.g. #13287.
|
|
of a match.
Reviewed-by: ppedrot
|
|
|
|
This was deactivated in fb1c2a017e but it seems useful (e.g. in
contribs containers).
It seems to be useful
|
|
Reviewed-by: gares
|
|
Also some dead code.
If no typo is introduced, there should be no semantic changes.
|
|
Ideally, if equations t <= ?x were preserving subtyping that could be
simpler. Currently we need however to put a rigid universe as
constraint on the return predicate so that one branch does not force
the return sort to be lower by unification than what another branch
would have needed.
|
|
If the result is in SProp, Prop or (impredicative) Set, we preserve
this information since the elimination sort might be restricted by the
sort of the destructed type.
If the result is in Type, we use a fresh sort upper bound so that we
are sure not having residual algebraic universes which would raise
problems in a type constraint (e.g. in define_evar_as_product).
This fixes the part of #13278 posted on discourse.
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: ejgallego
|
|
pattern-matching clause with unused named variable
Reviewed-by: jfehrle
Reviewed-by: vbgl
Ack-by: gares
|
|
|
|
|
|
This is similar to Constant and MutInd but for some reason this was was never
done. Such a patch makes the whole API more regular. We also deprecate the
legacy aliases.
|
|
|
|
|
|
This allows to quickly spot the parts of the code that rely on the canonical
ordering. When possible we directly introduce the quotient-aware versions.
|
