| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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...
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The type `raw_cases_pattern_expr` is used only in the interpretation
of notation patterns. Indeed, this should be a private type thus we
make it local to `Constrintern`; it makes no sense to expose it in the
public AST.
The patch is routine, except for the case used to interpret primitives
in patterns. We now return a `glob_constr` representing the raw
pattern, instead of the private raw pattern type. This could be
further refactored but have opted to be conservative here.
This patch is a refinement of b2953849b999d1c3b42c0f494b234f2a93ac7754
, see the commentaries there for more information about
`raw_cases_pattern_expr`.
|
| | |
| |
| |
| | |
The addition to the test suite showcases the usage.
|
| | |\ |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
I'm sure this was pushed by accident, since testing shows immediately
that it breaks the compilation of the ssreflect plugin, hence all
developments relying on it in Travis.
|
| | | |
| | |
| | |
| | | |
A priori considered to be a good programming style.
|
| | |\ \
| | | |
| | | |
| | | | |
let-ins
|
| | | |/
| |/| |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Following @gasche idea, and the original intention of #402, we switch
the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast`
which is private and record-based.
This provides significantly clearer code for the AST, and is robust
wrt attributes.
|
| | | |
| | |
| | |
| | | |
Thanks to @gasche
|
| | | |
| | |
| | |
| | | |
Now it is a private field, locations are optional.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
We continue the uniformization pass. No big news here, trying to be
minimally invasive.
|
| | | |
| | |
| | |
| | |
| | | |
We continue the uniformization pass. No big news here, trying to be
minimally invasive.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is the second patch, which is a bit more invasive. We reasoning
is similar to the previous patch.
Code is not as clean as it could as we would need to convert
`glob_constr` to located too, then a few parts could just map the
location.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is first of a series of patches, converting `constrexpr` pattern
data type from ad-hoc location handling to `Loc.located`.
Along Coq, we can find two different coding styles for handling
objects with location information: one style uses `'a Loc.located`,
whereas other data structures directly embed `Loc.t` in their
constructors.
Handling all located objects uniformly would be very convenient, and
would allow optimizing certain cases, in particular making located
smarter when there is no location information, as it is the case for
all terms coming from the kernel.
`git grep 'Loc.t \*'` gives an overview of the remaining work to do.
We've also added an experimental API for `located` to the `Loc`
module, `Loc.tag` should be used to add locations objects, making it
explicit in the code when a "located" object is created.
|
| | | |
|
| |\ \ |
|
| | | |
| | |
| | |
| | | |
Also documenting how the implicit arguments by position are computed.
|
| | |/
|/|
| |
| |
| | |
There were actually no syntax for it, and I'm still unsure what good
syntax to give to it, even more that it would be useful to have one.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
We remove the camlp4 compatibility layer, and try to clean up
most structures. `parsing/compat` is gone.
We added some documentation to the lexer/parser interfaces that are
often obscured by module includes.
|
| | |\
| |/
|/| |
|
| |\ \ |
|
| | | |\ |
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is the good parts of PR #360.
IIUC, these vernacular were meant mostly for debugging and they are
not supposed to be of any use these days.
Back and join are still there not to break the testing infrastructure,
but some day they should go away.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is a patch fulfilling the relevant remark of Maxime that an
explicit information at the ML type level would be better than "cast
surgery" to carry the optional type of a let-in.
There are a very few semantic changes.
- a "(x:t:=c)" in a block of binders is now written in the more
standard way "(x:=c:t)"
- in notations, the type of a let-in is not displayed if not
explicitly asked so.
See discussion at PR #417 for more information.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Previously a union type was used for externing.
In particular, moving extended_glob_local_binder to glob_constr.ml.
|
| | | |
| | |
| | |
| | | |
RawLocal -> CLocal
|
| | | |
| | |
| | |
| | | |
This is a bit long, but it is to keep a symmetry with constr_expr.
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Aligned the type binder_data to the naming scheme used in (raw)
local_binder and Rel.Declaration.t. Made some code factorization.
Still to do: align type Glob_term.glob_binder to the Assum/Def format
too.
Note: this includes fix of anomaly with 'pat in cofix (dec77f282).
|
| |/ / |
|
| | |
| |
| |
| |
| |
| |
| | |
- Adding a better location in the "apply" on the fly pattern.
- Printing statement of lemma and of hypothesis.
Was suggested by discussion at wish report #5390.
|
| | |\
| |/
|/| |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
named in the original term.
Useful at least for debugging, useful to give a better message than
"this placeholder", even if in the loc is known in this case.
|
| |\ \
| |/
|/| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing
changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341.
It turns out that calling from fake_ide the STM commands that were removed
by this PR requires an extension of the XML protocol. So postponing the
integration.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
I think these commands never make a lot of sense on scripts other than
debugging and we have better methods now.
The last remaining command, used for the tty emulation has been renamed
to VtBack, but it should go away at some point too once the legacy
interfaces are removed.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
In addition to a priority, cleanup the interfaces for passing this
information as well. The pattern, if given, takes priority over the
inferred one.
We only allow Existing Instances gr ... gr | pri. for now, without
pattern, as before.
Make the API compatible to 8.5 as well.
|
| |\| |
|
| | |
| |
| |
| | |
generates garbage. So the comment is kept but it is not passed over to ocamldoc.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The main point of this change is to fix #3035: Avoiding trailing
arguments in the Arguments command, and related issues occurring in
HoTT for instance. When the "assert" flag is not specified, we now
accept prefixes of the list of arguments.
The semantics of _ w.r.t. to renaming has changed. Previously, it meant
"restore the original name inferred from the type". Now it means "don't
change the current name".
The syntax of arguments is now restricted. Modifiers like /, ! and
scopes are allowed only in the first arguments list.
We also add *a lot* of missing checks on input values and fix various
bugs.
Note that this code is still way too complex for what it does, due to
the complexity of the implicit arguments, reduction behaviors and renaming
APIs.
|
Matej Košík
Emilio Jesus Gallego Arias
Gaetan Gilbert
Maxime Dénès
Hugo Herbelin
Pierre-Marie Pédrot
Matthieu Sozeau