| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
Apparently it was not useful. I don't remember what I was thinking
when I added it.
|
| | |
|
| |
|
|
| |
We move the last 3 types to more adequate places.
|
| |
|
|
|
| |
We move the "flag types" to its use place, and mark some arguments
with named parameters better.
|
| |
|
|
|
| |
This gets `Tactypes` closer to `tactics/`, however some legacy stuff
blocks it in `proofs`. We consider that is satisfactory for now.
|
| |
|
|
|
| |
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
| | |
|
| |\ |
|
| | |
| |
| |
| | |
Most of it seems straightforward.
|
| |/
|
|
|
|
|
| |
We use an option type instead of returning a pair with a boolean. Indeed, the
boolean being true was always indicating that the returned value was unchanged.
The previous API was somewhat error-prone, and I don't understand why it was
designed this way in the first place.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |\
| |
| |
| | |
in CArray
|
| | | |
|
| | | |
|
| |/
|
|
|
|
|
| |
`Proof_global` is the main consumer of the flag, which doesn't seem to
belong to the AST as plugins show.
This will allow the vernac AST to be placed in `vernac` indeed.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Uses internal to Refiner remain.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
| |
`Vernacexpr` lives conceptually higher than `proof`, however,
datatypes for bullets and goal selectors are in `Vernacexpr`.
In particular, we move:
- `proof_bullet`: to `Proof_bullet`
- `goal_selector`: to a new file `Goal_select`
|
| |
|
|
|
|
|
|
|
|
|
|
| |
We add a [SelectAlreadyFocused] constructor to [goal_selector] (read
"!") which causes a failure when there's not exactly 1 goal and
otherwise is a noop.
Then [Set Default Goal Selector "!".] puts us in "strict focusing"
mode where we can only run tactics if we have only one goal or use a
selector.
Closes #6689.
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
terms whose branches are in eta-let-expanded canonical form.
This is a hack intended to work only with destruct/case as they are
currently implemented. Would not work with arbitrary proofs of the
form "Cases(ci,p,c,[|...;b;...|] given to logic.ml for which b, if
with Metas, has not the form of an eta-let-expanded Meta.
|
| |/
|
|
|
|
|
| |
The V82 compatibility layer of the proof engine was used by cc
(congruence closure) for the sole purpose of maintaining an
environment and a sigma. We inline the corresponding env and sigma in
the state of cc algorithm to get rid of the compatibility layer.
|
| |
|
|
|
|
|
|
|
|
|
| |
We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:
- module declarations
- intro patterns
- top-level sentences
Now, parsed documents should be full annotated by `CAst` nodes.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
More precisely, we check that future goals retrieved in run_tactic
have no given_up goals since given_up goals are supposed to be
produced only by Proofview.given_up and put on the given_up store.
Doing the same for the shelf does not work: there is a situation where
run_tactic ends where the same goal is both in the comb and on the
shelf. This is when calling "clear x" on a goal "x:A |- ?p:B(?q[x])"
when the dependent goal "x:A |- ?q:C" is not on the shelf. Tactic
"clear" creates "|- ?p':B(?q'[])" and "|- ?q':C". The "advance" thing
sees that the new comb is now composed of ?p' and ?q' but ?q' is a
future goal which is later collected on the shelf (which ?q' is also
in the comb).
I tried to remove this redundancy but apparently it is
necessary. There is an example in HoTT (file
Classes/theory/rational.v) which requires this redundancy. I did not
investigate why: the dependent evar is created by ring as part of a
big term.
So, as a conclusion, I kept the redundancy.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Tactic-in-term can be called from within a tactic itself. We have to
preserve the preexisting future_goals (if called from pretyping) and
we have to inform of the existence of pending goals, using
future_goals which is the only way to tell it in the absence of being
part of an encapsulating proofview.
This fixes #6313.
Conversely, future goals, created by pretyping, can call ltac:(giveup) or
ltac:(shelve), and this has to be remembered. So, we do it.
|
| | |
|
| | |
|
| |
|
|
| |
UState normalize -> minimize, Evd nf_constraints -> minimize_universes
|
| | |
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | |/
|/| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.
With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.
|
| |/ |
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
We organize the toplevel execution as a record and pass it
around. This will be used by future PRs as to for example decouple
goal printing from the classifier.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
| |
In current code, `Proofview.Goal.t` uses a phantom type to indicate
whether the goal was properly substituted wrt current `evar_map` or
not.
After the introduction of `EConstr`, this distinction should have
become unnecessary, thus we remove the phantom parameter from
`'a Proofview.Goal.t`. This may introduce some minor incompatibilities
at the typing level. Code-wise, things should remain the same.
We thus deprecate `assume`. In a next commit, we will remove
normalization as much as possible from the code.
|
| | |
|
| |
|
|
|
| |
When asking for a hint about bullets, we check
that there is an ongoing proof.
|
| |
|
|
|
|
|
| |
The main contender was the abstract tactic that was generating useless
constraints for polymorphic subproofs that happened to contain themselves
monomorphic subproofs. We had to fix the test-suite for one particular
corner-case instance that looked more like a bug than anything else.
|
| |\ |
|
| |\ \ |
|
Gaëtan Gilbert
Matthieu Sozeau
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Hugo Herbelin
Maxime Dénès
Théo Zimmermann
Enrico Tassi
Cyprien Mangin