| Age | Commit message (Collapse) | Author |
|---|
|
This feature makes it possible to tell type inference to type
applications of a global `foo` using typing information from the context
once the `n` first arguments are known.
The syntax is: `Arguments foo x y | z`.
Closes #7910
|
|
|
|
We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.
This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.
|
|
(same for solve_remaining_evars)
This is the standard way to use these functions, with 1 exception in
Unification.
|
|
|
|
This builds on the work on #8545.
|
|
This module contains:
- the former ExtraEnv in pretyping
- a few functions to traverse binders in pretyping.ml and cases.ml
- the part of pretyping dealing with genarg interpretation
The dependency of pretyping in an interpretation of names as names of
variables of identifier is now hidden in GlobEnv (no more explicit
"lvar" management in pretyping.ml). Similarly for the interpretation
of names as terms and for the interpretation of tactics-in-terms.
We keep empty_lvar in Glob_ops for compatibility, even though it is a
bit isolated there.
|
|
We move syntax for universes from `Misctypes` to `Glob_term`. There is
basically no reason that this type is there instead of the proper
file, as witnessed by the diff.
Unfortunately the change is not compatible due to moving a type to a
higher level in the hierarchy, but we expect few problems.
This change plus the related PR (#6515) moving universe declaration to
their proper place make `Misctypes` into basically an empty file save
for introduction patterns.
|
|
|
|
This commit was motivated by true spurious conversions arising in my
`to_constr` debug branch.
The changes here need careful review as the tradeoffs are subtle and
still a lot of clean up remains to be done in `vernac/*`.
We have opted for penalize [minimally] the few users coming from true
`Constr`-land, but I am sure we can tweak code in a much better way.
In particular, it is not clear if internalization should take an
`evar_map` even in the cases where it is not triggered, see the
changes under `plugins` for a good example.
Also, the new return type of `Pretyping.understand` should undergo
careful review.
We don't touch `Impargs` as it is not clear how to proceed, however,
the current type of `compute_implicits_gen` looks very suspicious as
it is called often with free evars.
Some TODOs are:
- impargs was calling whd_all, the Econstr equivalent can be either
+ Reductionops.whd_all [which does refolding and no sharing]
+ Reductionops.clos_whd_flags with all as a flag.
|
|
|
|
|
|
|
|
There don't really bring anything, we also correct some minor nits
with the printing function.
|
|
Also nicer error when the constraints are impossible.
|
|
Note the problem with `create_evar_defs`.
|
|
We do up to `Term` which is the main bulk of the changes.
|
|
To this extent we factor out the relevant bits to a new file,
ltac_pretype.
|
|
When we used to parse to a glob_sort but always give an empty list in
the GType case we can now parse directly to Sorts.family.
|
|
Use the functional interface understand_tcc instead.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Also taking into account a name in the return clause and in the
indices.
Note the double meaning ``bound as a term to match'' and ``binding in
the "as" clause'' when the term to match is a variable for all of
"match", "if" and "let".
|
|
|
|
|
|
Now it is a private field, locations are optional.
|
|
|
|
All functions where actually called with the second argument of the pending
problem being the current evar map. We simply remove this useless and
error-prone second component.
|
|
|
|
We make mli files look to what they were looking before the move to EConstr
by opening this module.
|
|
|
|
|
|
This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.
Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.
|
|
|
|
|
|
|
|
|
|
This avoids leakage of universes. Also makes
Program Lemma/Fact work again, it tries to solve the
remaining evars using the obligation tactic.
|
|
|
|
|
|
|
|
|
|
This is a minimal modification to the pretyping interface which allows
for toplevel fixed points to be accepted by the pretyper.
Toplevel co-fixed points are accepted without this. However (co-)fixed
point _nested_ inside a `Definition` or a `Fixpoint` are always checked
for guardedness by the pretyper.
|
|
|
|
|
|
|
