| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |
|
|
| |
of a break.
|
| |
|
|
|
| |
future goals).
Fixes #3757. Thanks to Hugo for helping pinpoint the issue.
|
| | |
|
| |
|
|
|
|
| |
defined and the file providing the primitives.
The datatypes are defined in [Proofview_monad], previous [Proofview_monad] is now called [Logic_monad] since it is more generic since the refactoring.
|
| |
|
|
| |
ret -> return, bind -> (>>=), etc… So that monads expose a [Monad.S] signature. Also Proofview now exposes the [Monad.S] signature directly rather than in a [Monad.S] subdirectory.
|
| |
|
|
| |
[on_advance] gave almost no gain in readability, while costing a closure.
|
| | |
|
| |
|
|
|
|
| |
dispatch.
Leads to clearer an more efficient code.
|
| |
|
|
| |
For optimisation purposes.
|
| | |
|
| | |
|
| |
|
|
| |
It is, after all, a generic function about lists.
|
| |
|
|
| |
combinators.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
The Unsafe module is for unsafe tactics which cannot be done without anytime soon. Whereas V82 indicates a function which we want to get rid of and that shouldn't be used in a new function.
|
| | |
|
| | |
|
| | |
|
| |
|
| |
As simple as this looks, there's been some quite subtle issues in doing this modification, there may be bugs left.
|
| | |
|
| | |
|
| |
|
|
| |
(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.
|
| |
|
|
|
| |
First step in removing the [Goal] module whose code is now essentially legacy.
Removes the cache attached to a goal, which was used to avoid unnecessary [nf_evar]. May have a performance cost, which is to be fixed later.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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...).
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
The more structured goal record type of CoqIDE is also useful for other
interfaces (in particular, for PIDE). To support this, the datatype was
factored out to the Proof module. In addition, the record gains a type
parameter, to allow interfaces to adapt the output to their needs.
To accommodate this type, the Proof module also gains the
map_structured_proof that takes a Proof.proof and a function on the
individual goals (in the context of an evar map) and produces a
structured goal based on the goal transformer.
|
Pierre-Marie Pédrot
Arnaud Spiwack
Hugo Herbelin
Enrico Tassi
Carst Tankink