| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
| |
I made a confusion between ltac: in constr and ltac: in tactics, the
one needing parentheses in v8.5 but the latter needing parentheses
only in trunk.
This reverts commit f5dc54519f2a62bab2f7b9059e8c3c8dc53619be.
|
| | |
|
| |
|
|
|
| |
Return an evar_map with the right universes, when there are no focused
subgoals or the proof is finished.
|
| |
|
|
|
|
|
|
|
| |
E.g., Inductive foo := mkFoo { bla : foo } allowed to define recursive
records with eta for which conversion is incomplete.
- Eta-conversion only applies to BiFinite inductives
- Finiteness information is now checked by the kernel (the constructor types
must be strictly non recursive for BiFinite declarations).
|
| |
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
Fixpoint/Definition.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
For instance, #4447 is now printed:
λ Ca Da : ℕAlg,
let (ℕ, ℕ0) := (Ca, Da) in
let (C, p) := ℕ in
let (c₀, cs) := p in
let (D, p0) := ℕ0 in
let (d₀, ds) := p0 in
{h : C → D & ((h c₀ = d₀) * (∀ c : C, h (cs c) = ds (h c)))%type}
: ℕAlg → ℕAlg → Type
|
| | |
|
| | |
|
| |
|
|
|
| |
Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
|
| | |
|
| |
|
|
|
|
| |
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.
|
Guillaume Melquiond
Hugo Herbelin
Matthieu Sozeau
Matthieu Sozeau
Pierre-Marie Pédrot
Maxime Dénès
Enrico Tassi
Lionel Rieg
Thomas Sibut-Pinote
Gregory Malecha
Clément Pit--Claudel
Arnaud Spiwack
Pierre Corbineau
Pierre Letouzey
Pierre Courtieu