| Age | Commit message (Collapse) | Author |
|---|
|
- It removes some redundancies.
- It fixes failures when destructing a term mentioning goal hypotheses
x1, ..., xn or a term which is a section variable x when this term
is in a type with indices, and the indices also occur in the type of
one of x1, ..., xn, or of x.
- It fixes non-respect of eliminator type when completing pattern possibly
given by a prefix.
- It fixes b2e1d4ea930c which was dealing with the case when the term
was a section variable (it was unfortunately also breaking some
compatibility about which variables variable were generalized in
induction and which variables were automatically cleared because
unselected).
|
|
|
|
|
|
|
|
|
|
occurrences: some uniformisation was not appropriate for "change").
|
|
|
|
|
|
[Info] command.
|
|
|
|
[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.
|
|
|
|
Some particular care needed to be taken to print aliases properly.
The printing of argument is just the generic printer for [genarg]. The trouble is that (apart from being incomplete), it does not know that it's printing Ltac arguments. As a consequence, the arguments are not properly quoted (e.g. if they are tactic expressions, they are not within [ltac:(...)].
|
|
Empirically it works better on some notations than on others and I have no idea why. I've seen notations not printing their arguments, for instance, and other printing perfectly.
|
|
Since PMP's intervention, the [TACTIC EXTEND] tactics are not uniform: some are syntax, and some are just an internal name for an Ltac definition. The latter kind prints an internal name. It may be better to avoid printing them in the trace altogether. But I haven't figured out how to detect that properly yet.
|
|
The printing uses the printer for interpreted tactics. It only works for tactics which are defined in the new style. There are still a few atomic tactics in tacinterp which are defined in [V82] style. Namely:
exact, apply, clear, rename, reduce, change, (mutual variant of) fix, (mutual variant of) cofix
These print placeholder names which are never reparsable and not as useful.
|
|
Re-add, in fact, since it was there in v8.3 but was dead code in v8.4 hence was deleted. It is necessary for printing info traces, however. A lot of the code had changed since v8.3, so adapting the code was non-trivial and some thing may be printed wrong.
It require re-adding a [tacexpr] argument to [gen_tactic_expr]. It had been made obsolete by the deletion of [pr_tactic] in v8.4 (even though printing [glob_tactic_expr] in a [tactic_expr] is only an approximation of the appropriate behaviour).
A new kind of argument, [delayed_constr], has made an appearance between v8.4 and trunk, and it differs from [constr] in the typed level. So it required its own parameter in [gen_tactic_expr]. At this point [delayed_constr] are printed in the globalised level because they are interpreted as closures. Maybe a better approximation is warranted.
Both in the printing of rewrite and induction, I changed a [pr_lconstr] (note the 'l') by a [pr_dconstr]. It is probably not quite correct, and may need fixing (adding a [pr_dlconstr] to [Pptactics] I guess?).
|
|
|
|
The name is chosen in accordance to Ltac's syntax. In particular [refine] prints as Ltac's refine, which is not entirely correct (Ltac's refine does some βι-reduction after refinement). Maybe it would be better to give make it clear that it is a different refine. Still in refine, the constr is printed without taking into account the new evars, which, apart from potentially getting the order of the goals wrong, prints new evars as ?x instead of ?[x]. A printer for terms with new evars will be necessary.
In the case of [V82.tactic], the name is just <unknown> because there is no way to retrieve any information. It won't appear in the first level of info in Ltac, however, if the user would require a deeper trace, he may see internal tactics (Tactics defined with TACTIC EXTEND also have weird, unparsable, internal names).
|
|
Hence dispatches are printed as dispatches rather than sequences.
|
|
Called with [Info n tac], runs [tac] and prints its info trace unfolding [n] level of tactic names ([0] for no unfolding at all).
|
|
|
|
clause; extended it so that an induction over "x" is considered
generic when the clause has the form "in H |-" (w/o the conclusion)
and x does not occur in the conclusion.
|
|
|
|
This is now a "like first" strategy iff there is no occurrences
selected in either the goal or in one of the hypotheses possibly given
in an "in" clause. Before, it was "like first" if and only if no "in"
clause was given at all.
|
|
|
|
Need some contorsion for not using the general scheme of naming based
which uses the hypothesis name as base ident, and for instead keeping
a name generated on the type of the section variable, as it was before
for section variables (example of incompatibility in FMapPositive).
|
|
PIDE based GUIs can take advantage of multiple panels and get
some feedback routed there. E.g. query panel
|
|
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).
|
|
- proofworkertop to deal with proof tasks
- tacworkertop to deal with par: tactics
- queryworkertop to deal with queries (next commit)
|
|
|
|
|
|
|
|
When Coq's Haskell extraction needs to use unsafeCoerce, it passes
the -fglasgow-exts option to GHC, but recent versions of GHC warn
against this:
xx.hs:1:16: Warning:
-fglasgow-exts is deprecated: Use individual extensions instead
This patch does as the warning suggests, replacing -fglasgow-exts
with the specific option that the extraction needs (-XMagicHash).
|
|
When Haskell extraction requires magic type coersion, Coq produces
the following code:
unsafeCoerce :: a -> b
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
import qualified IOExts
unsafeCoerce = IOExts.unsafeCoerce
#endif
GHC version 7.6.3 does not allow imports after a type declaration,
and produces this error:
xx.hs:20:1: parse error on input `import'
(referring to the first import statement above). This patch moves
the unsafeCoerce type declaration to just after the import statement,
fixing this compile error.
|
|
|
|
|
|
|
|
|
|
|
|
Its semantics was dubious, and it was not used anymore anyway.
|
|
|
|
- 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).
|
|
|
|
|
|
|
|
keeping them as open holes. When these arguments are class instances,
this restores compatibility with the 8.4 search for subterms from
non-fully applied patterns which was using conversion on the
instances.
|
|
dependent in the goal without being fully applied: it cannot be
erased. This used to work in 8.4 when the hypothesis was in an empty
type. I fixed this and (somehow arbitrarily) generalized the
non-erasing to other inductive types instead of failing.
|
|
|
|
|
