| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |/
|/| |
|
| | |
|
|\ \ |
|
| | |
| | |
| | |
| | | |
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.
|
|\| |
|
| |
| |
| |
| | |
Also getting rid of a global side-effect.
|
|\ \ |
|
| |/
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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 *)
|
| |\
| | |
| | |
| | |
| | | |
Was PR#299: Fix bug #4869, allow Prop, Set, and level names in
constraints.
|
| | |
| | |
| | |
| | |
| | |
| | | |
This is a quick fix. The Metasyntax module should be thoroughly revised
in trunk, because it starts featuring a lot of spaghetti code and redundant
data.
|
| | |
| | |
| | |
| | |
| | | |
It seems warnings are not taken into account in output/
tests.
|
| |/ |
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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".
|
| | |
|
| | |
|
| | |
|