| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
Unfortunately OCaml doesn't deprecate the constructors of a type when
the type alias is deprecated.
In this case it means that we don't get rid of the kernel dependency
unless we deprecate the constructors too.
|
| |/
|
|
| |
One less global flag.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Virtually all classifications of vernacular commands (the STM
classifier, "filtered commands", "navigation commands", etc.) were
broken in presence of control vernaculars like Time, Timeout, Fail.
Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac
Debug in CoqIDE.
This change introduces a type separation between vernacular controls and
vernacular commands, together with an "under_control" combinator.
|
| |\
| |
| |
| | |
same right-hand side.
|
| | |
| |
| |
| | |
This is to have a better symmetry between CCases and GCases.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
In the transition towards a less global state handling we have the
necessity of mix imperative setting [notably for the modules/section
code] and functional handling of state [notably in the STM].
In that scenario, it is very convenient to have typed access to the
Coq's `summary`. Thus, I reify the API to support typed access to the
`summary`, and implement such access in a couple of convenient places.
We also update some internal datatypes to simplify the `frozen` data
type. We also remove the use of hashes as it doesn't really make
things faster, and most operations are now over `Maps` anyways.
I believe this goes in line with recent work by @ppedrot.
We also deprecate the non-typed accessors, which were only supposed to
be used in the STM, which is now ported to the finer primitives.
|
| |
|
|
|
|
|
|
| |
They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced
|
| |
|
|
|
|
|
|
|
|
| |
We remove deprecated syntax "Coercion Local" and such, and seize the
opportunity to refactor some code around vernac_expr.
We also do a small fix on the STM classification, which didn't know about
Let Fixpoint and Let CoFixpoint.
This is a preliminary step for the work on attributes.
|
| |\
| |
| |
| | |
of levels
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
Was introduced in 0917ce7c to fix #4272, but it seems that we can fix
it by just merging levels 10 and 11. This prevents the worry of fixing
the associativity of level 11 to left in 0917ce7c.
|
| | |
| |
| |
| |
| |
| | |
Apparently a long-standing bug, coupled with a pattern/constr
associativity inconsistency introduced while fixing another
pattern/constr level inconsistency (bug #4272, 0917ce7c).
|
| |/ |
|
| |\
| |
| |
| | |
separator
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This addresses a limitation found in math-comp seq.v file. See the example in
test suite file success/Notations2.v.
To go further and accept recursive notations with a separator made of
several tokens, and assuming camlp5 unchanged, one would need to
declare an auxiliary entry for this sequence of tokens and use it as
an "atomic" (non-terminal) separator. See PR #6167 for details.
|
| | |/
| |
| |
| | |
Replaced by ident_decl in #688.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
| |
Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to
put any pattern in binders, prefixed by a quote."] its current
placement as well as the hook don't make a lot of sense.
In particular, they prevent parts of Coq working without linking the
parser.
To this purpose, we need to consolidate the `Constrexpr`
utilities. While we are at it we do so and remove the `Topconstr`
module which is fully redundant with `Constrexpr_ops`.
|
| |
|
|
| |
4.02.3 has been the minimal OCaml version for a while now.
|
| | |
|
| |
|
|
|
|
|
|
|
| |
We place `Proof_using` in the proper place [`vernac`] and we remove
gross parsing hacks.
The new placement should allow to use the printers and more convenient
structure, and reduce strange coupling between parsing and internal
representation.
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
"_something")
|
| | | |
| | |
| | |
| | |
| | | |
This includes _ and insecable space which can be used in idents and
this allows more precise heuristics.
|
| | |/
|/| |
|
| |\ \
| | |
| | |
| | | |
3e70ea9c.
|
| |\ \ \ |
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | | |
We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.
Next step, understand why.
|
| |/ /
| |
| |
| |
| | |
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
|
| |\ \ |
|
| | |/
|/|
| |
| |
| |
| |
| |
| | |
Unfortunately, some manual synchronization is needed between the
constr parser and the table of constr/pattern levels.
We do this synchronization which was missing in the commit moving
"x -> y" to a user-level notation.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof. By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.
Declarations of universe binders and constraints also works for
monomorphic definitions.
|
| |/ |
|
| |\
| |
| |
| | |
top of the linking chain.
|
| |\ \
| | |
| | |
| | | |
from location in file
|
| |\ \ \ |
|
| | | | | |
|
| | |/ /
| | |
| | |
| | |
| | | |
When we used to parse to a glob_sort but always give an empty list in
the GType case we can now parse directly to Sorts.family.
|
| | | |
| | |
| | |
| | | |
linking chain.
|
| | |/
|/|
| |
| | |
This removes a dependency from `G_vernac` to `Metasyntax`.
|
| |/
|
|
|
|
|
| |
These hacks to warn the users about needed modules are not needed
anymore in 8.8, as the proper error message is done in 8.7 already.
This helps in avoiding a dependency from parsing to MlTop.
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
restructuration
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This allows to issue a more appropriate message when a notation with a
{ } cannot be defined because of an incompatible level. E.g.:
Notation "{ A } + B" := (sumbool A B) (at level 20).
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
- Formerly, notations such as "{ A } + { B }" were typically split
into "{ _ }" and "_ + _". We keep the split only for parsing, which
is where it is really needed, but not anymore for interpretation,
nor printing.
- As a consequence, one notation string can give rise to several
grammar entries, but still only one printing entry.
- As another consequence, "{ A } + { B }" and "A + { B }" must be
reserved to be used, which is after all the natural expectation,
even if the sublevels are constrained.
- We also now keep the information "is ident", "is binder" in the
"key" characterizing the level of a notation.
|
| |\ \ \ |
|
Maxime Dénès
Emilio Jesus Gallego Arias
Hugo Herbelin
Matthieu Sozeau
Gaëtan Gilbert
Pierre-Marie Pédrot
Gaëtan Gilbert