| Age | Commit message (Collapse) | Author |
|---|
|
|
|
The command [Redirect "filename" (...)] redirects all the output of
[(...)] to file "filename.out". This is useful for storing the results of
an [Eval compute], for redirecting the results of a large search, for
automatically generating traces of interesting developments, and so on.
|
|
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.
|
|
|
|
|
|
Backported from trunk.
|
|
|
|
universe-polymorphism mode.
|
|
|
|
|
|
help).
|
|
|
|
|
|
Of course such proofs cannot be processed asynchronously
|
|
|
|
We build the rich XML at once without generating the printed string.
|
|
|
|
|
|
|
|
Furthermore, ML tactic dispatch is not done according to the
type of its argument anymore.
|
|
This will allow to get rid of the fragile mechanism of discriminating which
entry to call depending on the dynamic type of its arguments.
|
|
printing functions touched in the kernel).
|
|
printing functions touched in the kernel).
|
|
constr for primitive records (not used anywhere else than printing).
Problem reported by P. LeFanu Lumsdaine on HoTT/HoTT.
Also add some minor fixes in detyping and pretty printing related to universes.
|
|
|
|
After this commit, module_type_body is a particular case of module_type.
For a [module_type_body], the implementation field [mod_expr] is
supposed to be always [Abstract]. This is verified by coqchk, even
if this isn't so crucial, since [mod_expr] is never read in the case
of a module type.
Concretely, this amounts to the following rewrite on field names
for module_type_body:
- typ_expr --> mod_type
- typ_expr_alg --> mod_type_alg
- typ_* --> mod_*
and adding two new fields to mtb:
- mod_expr (always containing Abstract)
- mod_retroknowledge (always containing [])
This refactoring should be completely transparent for the user.
Pros: code sharing, for instance subst_modtype = subst_module.
Cons: a runtime invariant (mod_expr = Abstract) which isn't
enforced by typing. I tried a polymorphic typing of mod_expr,
to share field names while not having mtb = mb, but the OCaml
typechecker isn't clever enough with polymorphic mutual fixpoints,
and reject code sharing (e.g. between subst_modtype and subst_module).
In the future (with ocaml>=4), some GADT could maybe help here,
but for now the current solution seems good enough.
|
|
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.
|
|
there is no focused goal.
The 'g' is for "global". The arguments are the same as [fail]. Beware: [let x := constr:… in tac] is a goal-local operation regardless of whether [tac] is goal-local or not.
|
|
This was due to the unqualified uses of "Lazy" being disambiguated in different manners. I just changed the constructor name to "Select".
Fixes #3877.
|
|
[multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well.
|
|
|
|
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.
|
|
|
|
[tryif t then t2 else t3] behaves like [t;t2] if [t] has at least one success, or [t3] otherwise. It generalises [t||t3] as failures from [t2] will not be caught.
|
|
You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
|
|
Documentation also updated.
|
|
Still to do:
- Decide between using SeveralInstancesFound or raising an error when
multiple instances exist.
- Use a proper printer for evars instead of the debugging
pr_evar_map_filter printer in pr_constraints.
|
|
|
|
|
|
|
|
|
