| Commit message (Collapse) | Author | Age |
| |
|
| |
|
|
|
|
|
| |
Now the seff contains it directly, no need to force the future
or to hope that it is a Direct opaque proof.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Before this patch opaque tables were only growing, making them unusable
in interactive mode (leak on Undo).
With this patch the opaque tables are functional and part of the env.
I.e. a constant_body can point to the proof term in 2 ways:
1) directly (before the constant is discharged)
2) indirectly, via an int, that is mapped by the opaque table to
the proof term.
This is now consistent in batch/interactive mode
This is step 0 to make an interactive coqtop able to dump a .vo/.vi
|
|
|
|
|
| |
The leafs of the XML trees are still pretty-printed strings, but this
could be refined later on.
|
| |
|
|
|
|
|
|
|
|
| |
will name the goal id; writing ?[?id] will use the first
fresh name available based with prefix id.
Tactics intro, rename, change, ... from logic.ml now preserve goal
name; cut preserves goal name on its main premise.
|
|
|
|
| |
It is not 100% complete, but the main part is there.
|
|
|
|
|
|
|
|
|
|
|
| |
so that one can retrieve them and pass them to third party tools (i.e.
print the AST with the notations attached to the nodes concerned).
Available syntax:
- all in one:
Notation "a /\ b" := ... (format "...", format "latex" "#1 \wedge #2").
- a posteriori:
Format Notation "a /\ b" "latex" "#1 \wedge #2".
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
Used to work "by chance".
|
| |
|
| |
|
|
|
| |
Dead code formerly used by the now defunct [autoinstances].
|
|
|
|
| |
Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
|
| |
|
| |
|
|
|
|
| |
stm test-suite files.
|
|
|
|
|
| |
par: distributes the goals among a number of workers given
by -async-proofs-tac-j (defaults to 2).
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
This is useful if a UI does not support that
|
| |
|
| |
|
|
|
|
|
| |
LoadedFile is generated when a .vo is loaded
Goals is generated when -feedback-goals
|
| |
|
| |
|
|
|
|
| |
These are now sufficient to implement PIDE
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
lib/interface split into:
- lib/feedback
subscribe-based feedback bus (also used by coqidetop)
- ide/interface
definition of coqide protocol messages
lib/pp
structured info/err/warn messages
lib/serialize split into:
- lib/serialize
generic xml serialization (list, pairs, int, loc, ...)
used by coqide but potentially useful to other interfaces
- ide/xmlprotocol
serialization of protocol messages as in ide/interface
the only drawback is that coqidetop needs -thread
and I had to pass that option to all files in ide/
|
|
|
|
|
|
|
|
|
|
|
|
| |
User interface writers can drop a footop.cmxs in $(COQLIB)/toploop/
and pass -toploop footop to customize the coq main loop.
A toploop must set Coqtop.toploop_init and Coqtop.toploop_run to
functions respectively initializing the toploop (and parsing toploop
specific arguments) and running the main loop itself.
For backward compatibility -ideslave and -async-proofs worker do
set the toploop to coqidetop and stmworkertop respectively.
|
|
|
|
| |
Every time you use abstract a kitten dies, please stop.
|
|
|
|
|
|
| |
and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml.
The context produced by typechecking a statement is passed in the proof, allowing the
universe name context to be correctly folded as well. Mainly an API cleanup.
|