| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
We artificially restrict the syntax though, because it is unclear of
what the semantics of several axioms in a row is, in particular about the
resolution of remaining evars.
|
| |
|
|
|
| |
These options can be set to a string value, but also unset.
Internal data is of type string option.
|
| |
|
|
|
|
|
|
|
| |
This option disallows "declare at first use" semantics for universe
variables (in @{}), forcing the declaration of _all_ universes appearing
in a definition when introducing it with syntax Definition/Inductive
foo@{i j k} .. The bound universes at the end of a definition/inductive
must be exactly those ones, no extras allowed currently.
Test-suite files using the old semantics just disable the option.
|
| | |
|
| |
|
|
| |
Seems to be morally required since we have the -type-in-type flag.
|
| |
|
|
|
| |
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
|
| |
|
|
|
| |
Correcting the code w.r.t. to the API was not the right solution. Instead,
the API comment had to be corrected.
|
| |
|
|
|
|
| |
We ensure statically by typing that the tags used by the rich printer
are integers. Furthermore, we also expose through typing that tags are
irrelevants in the returned XML.
|
| | |
|
| |
|
|
| |
"Print Module command shows module type expression incorrectly".
|
| |
|
|
| |
They do not have eta-rule indeed, even though it was displayed as such.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| | |
|
| |
|
|
| |
This allows fatal_error to be used for printing anomalies at loading time.
|
| |
|
|
|
| |
Fixes bug 3936
This closes #73
|
| |
|
|
|
| |
Ideally, the code should be shared between the various toplevels, but this
is a lot more work than just fixing a few strings.
|
| |
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
| |
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.
|
Pierre-Marie Pédrot
Enrico Tassi
Matthieu Sozeau
Maxime Dénès
Lionel Rieg
Thomas Sibut-Pinote
Gregory Malecha
Guillaume Melquiond
Clément Pit--Claudel
Arnaud Spiwack
Pierre Corbineau
Hugo Herbelin
Matthieu Sozeau
Pierre Letouzey
Pierre Courtieu