| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
| |
inductive types (i.e., ones declared with an explicit anonymous Type
at the conclusion of their arity). With this change one can force
inductives to live in higher universes even in the non-fully universe
polymorphic case (e.g. bug #3821).
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Do use the flag for_ml for distinguishing coq level and ml level
ltac definitions.
- Skip ML call from the trace.
There are still differences from 8.4 and trunk. For instance on:
Ltac f x := refine x.
Goal False.
f I.
8.4 says:
In nested Ltac calls to "f" and "x" (with x:=I), last term evaluation failed.
Error: The term "I" has type "True" while it is expected to have type "False".
trunk says:
In nested Ltac calls to "f" and "refine <genarg:uconstr>", last call failed.
Error: The term "I" has type "True" while it is expected to have type "False".
Maybe we would like a mix of both (besides the printing of a
non-elegant "<genarg:uconstr>)?
|
| |
|
|
| |
with evars.
|
| | |
|
| |
|
|
| |
[Set Info Level n] prints all info traces at level [n]. [Unset Info Level] stops the automatic printing of info traces. The unfolding level [n] can be overloaded by local [Info m tac] calls.
|
| |
|
|
| |
Called with [Info n tac], runs [tac] and prints its info trace unfolding [n] level of tactic names ([0] for no unfolding at all).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
With the options -async-queries-always-delegate queries are
always delegated to a worker process (Eval, Check, ...).
Users of PIDE based UIs (in Denmark) reported that the current
behavior of processing query synchronously is rather unexpected
when one is used to get proofs processed asynchronously.
Non instantaneous queries are part of many scripts and are there
as "tests" for testing the execution of recursive functions.
A standard proof script shape in an ongoing work by Appel and Bengtson
is made of blocks like:
- recursive function definition,
- some tests,
- some proofs
And one cannot quickly jump over the tests (only the proofs).
Enclosing the queries into dummy proofs to recover a reactive UI
is just annoying. Hence this patch.
Currently CoqIDE is not able to integrate the asynchronous feedback
of the query workers into the document, hence if one passes the option
to CoqIDE one only gets a boolean out of queries (processed/error).
|
| | |
|
| |
|
|
|
|
|
| |
- Show does not print the goal twice
- Undo is considered as part of the document when PG mode
(bug introduced when Undo was said not to be part of the document in
coqtop mode).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The main change is that selection of subterm is made similar whether
the given term is fully applied or not.
- The selection of subterm now works as follows depending on whether
the "at" is given, of whether the subterm is fully applied or not,
and whether there are incompatible subterms matching the pattern. In
particular, we have:
"at" given
| subterm fully applied
| | incompatible subterms
| | |
Y Y - it works like in 8.4
Y N - this was broken in 8.4 ("at" was ineffective and it was finding
all subterms syntactically equal to the first one which matches)
N Y Y it now finds all subterms like the first one which matches
while in 8.4 it used to fail (I hope it is not a too risky in-draft
for a semantics we would regret...) (e.g. "destruct (S _)" on
goal "S x = S y + S x" now selects the two occurrences of "S x"
while it was failing before)
N Y N it works like in 8.4
N N - it works like in 8.4, selecting all subterms like the
first one which matches
- Note that the "historical" semantics, when looking for a subterm, to
select all subterms that syntactically match the first subterm to
match the pattern (looking from left to right) is now internally called
"like first".
- Selection of subterms can now find the type by pattern-matching (useful e.g.
for "induction (nat_rect _ _ _ _)")
- A version of Unification.w_unify w/o any conversion is used for
finding the subterm: it could be easily replaced by an other
matching algorithm.
In particular, "destruct H" now works on a goal such as "H:True -> x<=y |- P y".
Secondary change is in the interpretation of terms with existential
variables:
- When several arguments are given, interpretation is delayed at the
time of execution
- Because we aim at eventually accepting "edestruct c" with unresolved
holes in c, we need the sigma obtained from c to be an extension of
the sigma of the tactics, while before, we just type-checked c
independently of the sigma of the tactic
- Finishing the resolution of evars (using type classes, candidates,
pending conversion problems) is made slightly cleaner: it now takes
three states: a term is evaluated in state sigma, leading to state
sigma' >= sigma, with evars finally solved in state sigma'' >=
sigma'; we solve evars in the diff of sigma' and sigma and report
the solution in sigma''
- We however renounce to give now a success semantics to "edestruct c"
when "c" has unresolved holes, waiting instead for a decision on
what to do in the case of a similar eapply (see mail to coqdev).
An auxiliary change is that an "in" clause can be attached to each component
of a "destruct t, u, v", etc.
Incidentally, make_abstraction does not do evar resolution itself any longer.
|
| |
|
|
|
|
| |
an updated evar_map, as pattern is working up to universe equalities
that must be kept. Straightforward adaptation of the code depending on
this.
|
| | |
|
| |
|
|
|
|
| |
Cd can make the relative path of the opened file wrong,
and hence not available anymore when we reopen it to compute
the line number.
|
| |
|
|
|
|
|
|
|
|
| |
Goal printing was partially broken. Some commands in vernacentries
were printing, but not all of them. Moreover an unlucky combination
of `Flags.verbosely (fun () -> interp "Set Silent")` was making the
silent flag not settable anymore.
Now STM always print the open goals after a command when run in interactive
mode via coqtop or emacs. More modern GUI do ask for the goals.
|
| |
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
|
|
| |
That is [Tactics.New.refine]. Replaced it with a wrapper around the primitive refine [Proofview.Refine.refine], but with extra reductions on the resulting goals.
There was two used of this refine: one in the declarative mode, and one in type classes. The porting of the latter is likely to have introduced bugs.
Factored code with Ltac's refine in Extratactics.
|
| |
|
| |
As simple as this looks, there's been some quite subtle issues in doing this modification, there may be bugs left.
|
| |
|
|
|
|
| |
Check (see cfff8f8a327) [printing only visible evars, not the ones
corresponding to unrelated open goals + fixing bug on wrong sigma and
on evar_info normalization].
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| | |
|
| |
|
|
|
|
|
| |
for the record binder of classes. This name is no longer generated
in the kernel but part of the declaration. Also cleanup the interface
to recognize primitive records based on an option type instead of a
dynamic check of the length of an array.
|
| |
|
|
|
| |
projections and regular records.
Easily fixable backwards incompatibility.
|
| |
|
|
| |
and unsatisfiable constraints which were not done in the right environment.
|
| |
|
|
|
|
| |
being able to export hints without tactics, vm, etc. to come with.
Some functions moved to the new proof engine.
|
| | |
|
| |
|
|
| |
scope" error message).
|
| |
|
|
|
|
|
|
| |
inductives).
The implementation constant should have the a universe instance
of the same length, we assume the universes are in the same order
and we check that the definition does not add any constraints
to the expected ones. This fixes bug #3670.
|
| |
|
|
|
|
| |
Was just printed in the case of internal holes.
Also: replace [str] by [strbrk] in error message of unsolved holes for better layout.
|
| | |
|
| |
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
| |
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".
|
| | |
|
Matthieu Sozeau
Hugo Herbelin
Pierre-Marie Pédrot
Xavier Clerc
Enrico Tassi
Arnaud Spiwack