| Commit message (Collapse) | Author | Age |
|\
| |
| |
| | |
constants
|
| |
| |
| |
| |
| | |
Apparently it was not useful. I don't remember what I was thinking
when I added it.
|
|\ \
| |/
|/| |
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | | |
The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.
|
|/ /
| |
| |
| |
| |
| |
| |
| | |
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.
|
|/
|
|
| |
Avoid adding the same unification problem twice, module evar instantiation.
|
|
|
|
|
| |
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
| |
|
| |
|
|\ |
|
|\ \ |
|
| | |
| | |
| | | |
Actually all the new_ functions are in evarutil still
|
| |/
|/| |
|
|\ \ |
|
| | |
| | |
| | |
| | | |
Most of it seems straightforward.
|
| |/
|/|
| |
| | |
Note that `Assumptions` ships its own copy, but for `Constr.t`.
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |/
|/| |
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | | |
We now have only two notions of environments in the kernel: env and
safe_env.
|
|/ /
| |
| |
| | |
We address the easy ones, but they should probably be all removed.
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
This finishes the splitting of Universes.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
This API is a bit strange, I expect it will change at some point.
|
| | |
|
|\ \ |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | | |
clear_hyps remain with no alternative
|
|/ / |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
|\ \ |
|
|\ \ \ |
|
| | | | |
|
| |/ /
|/| | |
|
|\ \ \ |
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
indirect uses of tactic `clear`.
|
|\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
hypotheses.
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
- Be more precise when trying to clear an hypothesis which
occurs implicitly in a global constant.
- Warns if destruct/induction cannot clear an hypothesis occurring
implicitly in a global.
In the first case, the change in situation
Section A. Variable a:nat. Definition b:=a=a. Goal b=b. clear a.
is:
- before: "a is used in conclusion"
- after: "a is used implicitly in b in conclusion"
In the second case:
Section A. Variable a:nat. Definition b:=a=a. Goal b=b. destruct a.
produces a warning: "Cannot remove a, it is used implicitly in b".
|
| |/ / / /
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Four modes currently supported to deal with clashes:
1. Failing in case of clash
2. Renaming the most recent one
3. Renaming the previous hypothesis of same name if not a section variable
4. Renaming the previous hypothesis of same name even if a section variable
The current mode is 3. Keeping it active by default
|