| Age | Commit message (Collapse) | Author |
|---|
|
(More thinking needed)
|
|
Makes the monad more flexible as it will be easier to add new components to the concrete state of the tactic monad.
The Proofview module is also organised in a more abstract way with dedicated submodules to access various parts of the state or writer.
|
|
Changes in the implementation details had unwittingly changed the order in which Grab Existential Variables displayed the goals.
|
|
|
|
Uses the new architecture which allows to keep track of all new evars. The [future_goals] are flushed at the end of the tactics, the [principal_future_goal] is ignored.
|
|
In my first attempt I just dropped all future goals before starting a refinement. This was done for simplicity but is incorrect in general. In this version the future goals which are not introduced by the particular instance of refine are kept for future use.
|
|
Now [Goal] only contains a few helpers.
|
|
|
|
The rest will take more work.
|
|
We are left with the compatibility layer and a handful of primitives which require some thought to move.
|
|
|
|
Now, usual function from Evarutil are used to define evars instead of the variants from Proofview.Refine.
The [update] primitive which tried to patch the difference between pretyping functions and the refine primitive is now replaced by the identity function.
|
|
See previous commit for more discussion.
Changed the name from "main" to "principal" because I find "main" overused, and because the name was only introduced yesterday anyway.
|
|
That way, everything in the code of pretying is made "refine"-aware. Making the abstraction stonger and integration of pretyping with interactive proof more direct.
It might create goals in a slightly different goal order in the (user level) refine tactic. Because now, the [update] primitive which used to infer an order from an [evar_map] now has the order fixed by the successive declaration with [Evarutil.new_evar] (and similar). It probably coincides, though.
Following a suggestion by Hugo.
|
|
[refine].
This makes [new_evar] closer to be a mere wrapper around [Evarutil.new_evars]. Will allow restructuring of the refinement interface.
|
|
|
|
another one.
|
|
|
|
Refine.
|
|
Not very optimized though (if we apply convert_hyp on any hyp, a new
evar will be generated for every different hyp...).
|
|
|
|
|
|
- Removed collect_evars which does not consider instance
(use evars_of_term instead).
- Also removed evars_of_evar_info which did not filter context (use
evars_of_filterered_evar_info instead). This is consistent with
printing goal contexts in the filtered way.
Anyway, as of today, afaics goals filters are trivial
because (if I interpret evarutil.ml correctly), evars with
non-trivial filter necessarily occur in a conv pb. Conversely,
conv pbs being solved when tactics are called, there should not be
an evar used as a goal with a non-trivial filter.
|
|
Most of the code from Goal.Refine and related was moved to the one
file that was using it, wiz. tactics.ml. Some additional care should
be taken to clean up even more the remaining code.
|
|
|
|
Goals have to be refreshed when observed, because the evarmap may have
changed between the moment where the goal was generated and the moment the
goal is used.
|
|
All goals were normalised up front, rather than normalised after the tactic acting on previous goal had the chance to solve some evars, which then appeared non-instantiated to tactics which do not work up to evar map (most of them).
|
|
for tclEVARS which might solve existing goals.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
1. Proofview.Goal.enter into Proofview.Goal.nf_enter.
2. Proofview.Goal.raw_enter into Proofview.Goal.enter.
3. Proofview.Goal.goals -> Proofview.Goals.nf_goals
4. Proofview.Goal.raw_goals -> Proofview.Goals.goals
5. Ftactic.goals -> Ftactic.nf_goals
6. Ftactic.raw_goals -> Ftactic.goals
This is more uniform with the other functions of Coq.
|
|
This time it should work at least as well as the previous version. The error
messages were adapted a little. There is still a buggy behaviour when clearing
lets in section, but this is mostly a problem of section handling. The v8.4
version of clearbody did exhibit the same behaviour anyway.
|
|
Proofview goals coincide by always using the named context and discarding the
hypotheses.
|
|
In order not to be too costly, there is an [unsafe] flag to be set if the
tactic does not have to check that the partial proof term is well-typed (to
be used with caution though).
This patch breaks one [fix]-based example in the refine test-suite, but a huge
development like CompCert still goes through.
|
|
Hopefully, this may fix some nasty bugs lying around.
|
|
This allows to write a multigoal idtac without having to resort to
the hack of modifying the global environment tactic through tclIN_ENV,
which may cause trouble if we want to modify it in a state-passing style.
|
|
This reverts commit 664b3cba1e8d326382ca981aa49fdf00edd429e6.
Conflicts:
proofs/proofview.ml
|
|
This should allow tactics after a Goal.enter not to have to renormalize
them uselessly.
|
|
|
|
Some legacy code remains to keep the newish refine tactic working, but
ultimately it should be removed. I did not manage to do it properly though,
i.e. without breaking the test-suite furthermore.
|
|
|
|
Fixes PTSF (though I have no idea what caused this bug to show up just yesterday).
|
|
When "entering" in a goal, the environment observed by [tclENV] is changed (in the scope of the goal) to be that of the goal.
I'm not entirely sure it is the right semantics. But it allows to write tactics which are agnostic of whether they are run in a goal or not.
|
|
* Add comments in the code (mostly imported from Monad.v)
* Inline duplicated module
* Clean up some artifacts due to the extracted code.
* [NonLogical.new_ref] -> [NonLogical.ref] (I don't even remember why I chose this name originally)
* Remove the now superfluous [Proof_errors] module (which was used to define exceptions to be used in the extracted code).
* Remove Monad.v
|
|
The [num_goal] tactic counts the number of focused goals.
|
|
|
