| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
It used to be Stateid.initial by default. That is indeed a valid
state id but very likely not the very best one (that would be
the tip of the document).
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
PR#173 introduced a record field name clash in `stm.mli`, with duplicate
fields `start/stop` for the types `focus` and `static_block_declaration`.
We fix by renaming the younger ones (as to minimize code
incompatibilities), but other options are possible/could be preferred,
however they would be quite more invasive so I think they should be
postponed for the day the Stm API is cleaned up.
|
| |\| |
|
| |\ \ |
|
| | |/
| |
| |
| |
| |
| |
| |
| |
| |
| | |
For now, the only meaningful user is "Set Warnings". Example:
Section Bar.
Local Set Warnings Append "-foo".
(* warning foo is now disabled *)
End Bar.
(* foo is now reenabled, assuming it was before entering the section *)
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
When a proof is 're-opened', the Qed node does not change.
Still the STM has to install the old state (where only
the future proof has to be updated). This bit was missing.
Why was it working: the bug happens only if you
reopen the very last proof, i.e. there is no
sentence that stays valid after the Qed. If there
is such a sentence, its state was computed correctly
before, and is not changed. If it is the very last,
then the next state is based on the wrong one...
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
This avoids leakage of universes. Also makes
Program Lemma/Fact work again, it tries to solve the
remaining evars using the obligation tactic.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
I hadn't realized that this PR uses OCaml's 4.03 inlined records
feature. I will advocate again for a switch to the latest OCaml stable
version, but meanwhile, let's revert. Sorry for the noise.
This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing
changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
The new name makes it more obvious what is meant here by "kind". We leave
Decl_kinds.binding_kind as a deprecated alias for plugin
compatibility.
We also replace bool with implicit_status in a few places in the
codebase.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We get rid of tuples containing booleans (typically for universe
polymorphism) by replacing them with records.
The previously common idom:
if pi2 kind (* polymorphic *) then ... else ...
becomes:
if kind.polymorphic then ... else ...
To make the construction and destruction of these records lightweight,
the labels of boolean arguments for universe polymorphism are now
usually also called "polymorphic".
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
I think that a better place for the mutex would be the printing routine,
but I still hope we will get rid of threads in favor of coroutines.
So I keep all mutexes in Stm.
|
| |\ \ |
|
| |\ \ \
| | |/
| |/| |
|
| | |\ \ |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
There was an "optimization", since Abort is an empty side effect.
But that optimization had an impact on the DAG shape.
Now a nested proof, no matter if it is kept or dropped, is handled the same.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Using abstract can create beta-redexes or let-ins in the head of the
proof terms. The code projecting out mutual lemmas was not robust
enough.
|
| | | | |
| | | |
| | | |
| | | | |
So that a module can add his own and look at the traffic
|
| |\| | | |
|
| | |\| | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We add a flag Keep Admitted Variables that allows to recover the legacy
v8.4 behaviour of admitted lemmas. The statement of such lemmas did not
depend on the current context variables.
|
| | | | |
| | | |
| | | |
| | | | |
Fix done with Enrico.
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions.
If multiple modules define a function with a same name, e.g.:
Context.{Rel,Named}.get_type
those calls were prefixed with a corresponding prefix
to make sure that it is obvious which function is being called.
|
| | | |
| | |
| | |
| | | |
Suggested by @ppedrot
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
As noted by @ppedrot, the first is redundant. The patch is basically a renaming.
We didn't make the component optional yet, but this could happen in a
future patch.
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.
We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.
This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
|
| | |
| |
| |
| |
| |
| | |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is a reimplementation of Hugo's PR#117.
We are trying to address the problem that the name of some reduction functions
was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in
reduction). Like PR#117, we are careful that no function changed semantics
without changing the names. Porting existing ML code should be a matter of
renamings a few function calls.
Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX
collectively denominated iota.
We renamed the following functions:
Closure.betadeltaiota -> Closure.all
Closure.betadeltaiotanolet -> Closure.allnolet
Reductionops.beta -> Closure.beta
Reductionops.zeta -> Closure.zeta
Reductionops.betaiota -> Closure.betaiota
Reductionops.betaiotazeta -> Closure.betaiotazeta
Reductionops.delta -> Closure.delta
Reductionops.betalet -> Closure.betazeta
Reductionops.betadelta -> Closure.betadeltazeta
Reductionops.betadeltaiota -> Closure.all
Reductionops.betadeltaiotanolet -> Closure.allnolet
Closure.no_red -> Closure.nored
Reductionops.nored -> Closure.nored
Reductionops.nf_betadeltaiota -> Reductionops.nf_all
Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta
Reductionops.whd_betadeltaiota -> Reductionops.whd_all
Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet
Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack
Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack
Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack
Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state
Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state
Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state
Reductionops.whd_eta -> Reductionops.shrink_eta
Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all
Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all
And removed the following ones:
Reductionops.whd_betaetalet
Reductionops.whd_betaetalet_stack
Reductionops.whd_betaetalet_state
Reductionops.whd_betadeltaeta_stack
Reductionops.whd_betadeltaeta_state
Reductionops.whd_betadeltaeta
Reductionops.whd_betadeltaiotaeta_stack
Reductionops.whd_betadeltaiotaeta_state
Reductionops.whd_betadeltaiotaeta
They were unused and having some reduction functions perform eta is confusing
as whd_all and nf_all don't do it.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
When declaring the universes of a lemma explicitely, throw an error if
after minimization the type of a lemma still refers to unbound
universes. This is a fix and an incompatibility, but scripts
will be backwards compatible themselves.
Fix another minor bug in treating universe binders for (Co)Fixpoint.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The ErrorMsg datatype was introduced to allow locations in messages,
however, it was redundant with error and used only in one place.
We remove it in favor of a more uniform treatment of messages with
location. This patch also removes the use of `Loc.ghost` in one place.
Lightly tested.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This commit documents par:, fixes its semantics so that is
behaves like all:, supports (toplevel) abstract and optimizes
toplevel solve.
`par: solve [tac]` is equivalent to `Ltac tac1 := solve[tac]...par: tac1`
but is optimized for failures: if one goal fails all are aborted
immediately.
`par: abstract tac` runs abstract on the generated proof terms. Nested
abstract calls are not supported.
|
| | |
| |
| |
| |
| | |
This allows a smooth addition of various unsafe flags without wreaking
havoc in the ML codebase.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
We decided to only export the API, so that an external plugin can provide
this feature without having to merge it in current Coq trunk. This postpones
the attribute implementation in vernacular commands after 8.6.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is a minimal modification to the pretyping interface which allows
for toplevel fixed points to be accepted by the pretyper.
Toplevel co-fixed points are accepted without this. However (co-)fixed
point _nested_ inside a `Definition` or a `Fixpoint` are always checked
for guardedness by the pretyper.
|
| |\ \ \
| | | |
| | | |
| | | | |
Add -o option to coqc
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
Pierre-Marie Pédrot
Enrico Tassi
Emilio Jesus Gallego Arias
Guillaume Melquiond
Matthieu Sozeau
Maxime Dénès
Matej Kosik
Pierre Letouzey
Matthieu Sozeau
Arnaud Spiwack