| Age | Commit message (Collapse) | Author |
|---|
|
Return an evar_map with the right universes, when there are no focused
subgoals or the proof is finished.
|
|
The current solution may not be totally ideal though. We generate names for
anonymous evars on the fly at printing time, based on the Evar_kind data they
are wearing. This means in particular that the printed name of an anonymous
evar may change in the future because some unrelate evar has been solved or
introduced.
|
|
|
|
|
|
Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
|
|
|
|
Seems to be morally required since we have the -type-in-type flag.
|
|
When an axiom of an empty type is matched in order to inhabit
a type, do print that type (as if each use of that axiom was a
distinct foo_subproof).
E.g.
Lemma w : True.
Proof. case demon. Qed.
Lemma x y : y = 0 /\ True /\ forall w, w = y.
Proof. split. case demon. split; [ exact w | case demon ]. Qed.
Print Assumptions x.
Prints:
Axioms:
demon : False
used in x to prove: forall w : nat, w = y
used in w to prove: True
used in x to prove: y = 0
|
|
Ideally, the code should be shared between the various toplevels, but this
is a lot more work than just fixing a few strings.
|
|
Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
|
|
It will not work in CoqIDE though, which handles printing its own way. It's a general remark that we have many ways of printing things in Coq and we should look for a unified structured framework to be shared between interfaces.
|
|
|
|
This is meant to help integrate the printers of the declarative mode.
|
|
|
|
|
|
printing functions touched in the kernel).
|
|
|
|
fd98174afe6 about fixing hypothesis alpha-conversion strategy for
This completion of the reverting fixes #3905.
|
|
Had to put some hook in the handler of Proofview.NoSuchgoals.
Documentation updated. CHANGE updated.
|
|
Such printer is already in Termops
This reverts commit 5d6106a075b79abbb92b03bbca7b13a517cf4925.
|
|
I find it very odd not to have a pretty printer for terms than can
be called from *everywhere*. This commit sticks in Term a long spaghetti
to let Printer install a printing function.
|
|
I added a emacs_logger.
Still need to cleanup std_logger.
|
|
Fixes the idtac "string" not appearing in proofgeneral because
printined *before* the goal.
|
|
Since it displays together with the goal, it is better (for pg and
other interfaces probably) that they are in a different message.
|
|
|
|
|
|
|
|
The core is a "detyping" function for [closed_glob_constr]. Which interpretes the variable names according to the Ltac context, and apply the standard detyping procedure to typed terms in the closure.
|
|
|
|
|
|
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).
|
|
coqide to coqtop.
(Joint work with Pierre)
|
|
|
|
We are left with the compatibility layer and a handful of primitives which require some thought to move.
|
|
|
|
works correctly with an hypothesis of the context and knowing that
related bug #3204 had its own fix.
|
|
|
|
This prevented the message from being silent when jumping ahead in a file. Fixes #3636.
|
|
contortions in internalization/externalization. It uses a fully typed
version of detyping, requiring the environment, to move from
primitive projection applications to regular applications of
the eta-expanded version. The kernel is unchanged, and only
constrMatching needs compatibility code now.
|
|
|
|
|
|
|
|
in instances.
|
|
|
|
instances still to do). Using heuristics to name after the quantifier
name it comes. Also added a "sigma" to almost all printing functions.
|
|
|
|
|
|
|
|
|
|
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.
|
