| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
We are waiting for an upstream merge of a fix related to coq_makefile2.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | | |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which
this PR solves, I propose to remove support for non-synchronous
options.
It seems the few uses of `optsync = false` we legacy and shouldn't
have any impact.
Moreover, non synchronous options may create particularly tricky
situations as for instance, they won't be propagated to workers.
|
| | | |/ / |
|
| | |/ /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We'd like to cleanup the `proof_end` type so we can have a smaller
path in proof save. Note that the construction:
```
Goal Type.
⋮
Save id.
```
has to be handled by the STM in the same path as Defined (but with an
opaque flag), as `Save id` will alter the environment and cannot be
processed in parallel.
We thus try to simply such paths a bit, as complexity of `lemmas.ml`
seems like an issue these days. The form `Save Theorem id` doesn't
really seem used, and moreover we should really add a type of "Goal",
and unify syntax.
It is often the case that beginners try `Goal addnC n : n + 0 = n."
etc...
|
| | |/
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This fixes an inconsistency introduced in 554a6c806 (svn r12603) where
both interp_constr_with_bindings and interp_open_constr_with_bindings
were going through interp_open_constr (no type classes so as to not to
commit too early on irreversible choices, accepting unresolved holes).
We fix this by having interp_constr_with_bindings going to
interp_constr (using type classes and failing on unresolved evars).
The external impact is that any TACTIC EXTEND which refers to
constr_with_binding has now to decide whether it intends it to use
what the name suggest (using type classes and to fail if evars remain
unresolved), thus keeping constr_with_binding, or the actual behavior
which requires to use open_constr_with_bindings for strict
compatibility.
|
| | | |
|
| | |\
| | |
| | |
| | | |
tricks available to users
|
| | |\ \ |
|
| | | |/
| |/| |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
Note that [@@@ocaml.warning "-32"] caused an error with Drop.
It was put there because I didn't realise the warning was about a real issue.
|
| | |\ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This development of @bmsherman tests universe polymorphism and setoid
rewriting in type, and should build with v8.6 and trunk.
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | |/ / |
|
| | |\ \ |
|
| | | | | |
|
| | |\ \ \
| | | |/
| | |/| |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
`internal_ghost` was an artifact to ease porting of the ml4 rules. Now
that the location is optional we can finally get rid of it.
|
| | | | |
| | | |
| | | |
| | | | |
Now it is a private field, locations are optional.
|
| |/ / / |
|
| | |/
|/| |
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| | |\ |
|
| | | | |
|
| | | | |
|
| | |/ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
As suggested by @psteckler in #524 , we give more explicit information
about what is wrong.
We also provide some debug information for the possible dangerous case
of having the tip go out of sync with the real installed state (which
will make parsing fail if there was some changes to the parser).
We also fix a couple of typos noticed by Paul, thanks Paul.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
- We clean-up `Vernac` and make it use the STM API.
- Now functions in `Vernac` for use in the toplevel and compiler take
an starting `Stateid.t`.
- Duplicated `Stm.interp` entry point is removed.
- The XML protocol call `interp` is disabled.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Mainly due to notations, proof modes and plugins, parsing in Coq is
stateful, so we expose a state-aware parsing API in the STM.
This is a first move to unify all the parsing entry points in the Stm
and the toplevel, and allows STM clients to control their input stream
properly. This greatly helps for instance, with whole-document
parsing.
This commit supersedes PR#204.
|
| |\ \ \
| | | |
| | | |
| | | | |
record fields.
|
| |\ \ \ \
| |_|/ /
|/| | | |
|
| |\ \ \ \ |
|
| | | | | | |
|
| | | |\ \ \
| |_|/ / /
|/| | | | |
|
| |/ / / / |
|
Maxime Dénès
Emilio Jesus Gallego Arias
Enrico Tassi
Hugo Herbelin
Jason Gross
Pierre-Marie Pédrot
Jason Gross
Gaetan Gilbert
Théo Zimmermann
Paul Steckler
Matthieu Sozeau