| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
Not 100% sure about this one TBH, this function is messy.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
This behaviour seems a bit dubious and it is indeed not needed, also
such re-raises seem like they will mess with the backtrace.
|
|
|
|
Reviewed-by: maximedenes
|
|
so for instance
~~~coq
Set Printing All. Set Printing Universes.
Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= .
Lemma bla@{u v|u < v} : foo@{u v} -> False.
Proof. induction 1. Qed.
~~~
works.
|
|
|
|
The type of h is reconstructed to look as much as the initial type of
h as possible.
|
|
Instead of relying on the Coq_config immutable flag, we introduce an
initialization-only flag to govern the use of the native compiler. This
allows to make coqc passed with "-native-compiler no" behave as if it had
been configured without native compilation.
|
|
The patch is done in a minimal way. The hacks are turned into a new kind of
safer hacks, but hacks nonetheless. They should go away at some point, but
the current patch is focussed on the removal of Libobject cruft, not making
the dirty code of its upper-layer callers any cleaner.
|
|
~strict flag
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
There are no users in Coq but maybe some plugin wants it so don't
completely remove it
|
|
One should generally push contexts with ~strict:true when the context is a monomorphic one (all univs > Set) except for template polymorphic inductives (>= Prop) and ~strict:false for universe polymorphic ones (>= Set). Includes fixes from Gaëtan's and Emilio's reviews
|
|
containing letins.
Reviewed-by: ppedrot
|
|
|
|
Some calls are actually guarded by a check that the scheme is already in
the cache. There is no reason to generate dummy side-effects in that case.
|
|
|
|
|
|
This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
|
|
The manual was already saying that it was deprecated, but no warning was
emitted.
Fixes #10572
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
This statically ensures more invariants and moves a global declaration out
of this function.
|
|
This means return_proof is the only place where it can be produced.
We need to change the stm a bit as it keeps a pointer to a
[closed_proof_output] to join and to check if it failed, and it needs
a way to create a dummy in 1 case.
I'm not sure if this works correctly though, how to test?
We also inline the used bits of [return_proof ~allow_partial:true] in
[save_lemma_admitted] to get [Proof using] info. We could
alternatively expose the [closed_proof_output -> constr list]
projection. I think the code is easier to understand this way though,
as we don't have to read [return_proof] and figure out that the side
effect manipulation is ignored etc.
Note that the "this will warn" comment was outdated since
73daf37ccc7a44cd29c9b67405111756c75cb26a
|
|
Beware of 0. = -0. issue for primitive floats
The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.
|
|
We introduce a new module that registers the scheme information that
side-effects need, thus removing the hook from `Declare`.
As we may want to deprecate scheme side effects, there is no need to
design a general mechanism for this kind of registration for now.
Would we remove the scheme side-effects the scheme code could become
self-contained again.
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
Ack-by: herbelin
|
|
Add experimental "Show Proof" command to the toplevel that shadows
the current command in the parser (in coqtop and PG only).
Apply existing code to highlight diffs in the output
|
|
We use an `evar_map ref` even tho the modification the `evar_map` is
ignored.
I'm not sure if this is a bug or not, so I am making thus preserving
the behavior but making the what is going with the `evar_map` more
explicit.
|
|
|
|
Proof entries are low-level objects and should not be manipulated by
users directly, in particular as we want to unify all the code
around declaration of constants.
This patch doesn't bring by itself a lot of improvement, other than
setting the base where to extend the interface, however it already
points out some points of interest, and in particular the manipulation
of opacity done by `Derive` which can be quite problematic, and of
course the handling of delayed proofs.
So while this is a first step, IMHO it doesn't harm a lot having it in
place, but a lot more work will be needed, in particular regarding the
handling of delayed proofs.
To make `proof_entry` a fully abstract type, the remaining work is
focused on `abstract` and obligations, both of which do quite a few
hackery that will have to be migrated to the `Declare` API.
|
|
We factor some duplicate code, this is a step towards making the
`proof_entry` type abstract.
|
|
The code is self-contained and only used by commands; this also
highlights the several `Libobject.obj` registered for each
declaration.
|
|
The code is self-contained and only used by commands; this also
highlights the several `Libobject.obj` registered for each
declaration.
|
