| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This fixes #8401
Supersedes / closes #8407
Vernacular-command-registered numeral notations now live in the summary,
and the interpretation function for them is hard-coded.
Plugin-registered numeral notations are still unsynchronized, and only
the UIDs of these functions gets synchronized. I am not 100% sure why
this is fine, but the test-suite file working suggests that it is fine.
I think it is because worker delegation correctly handles
non-synchronized state which is declared at `Declare ML Module`-time.
This final commit changes the synchronization of numeral notations (and
deletes no-longer-used declarations in notation.mli that were introduced
temporarily in the last commit). Since the interpretation can now be
done in notation.ml, we no longer need to register unique ids for
numeral notation (un)interp functions, and can instead synchronize the
underlying constants with the document state. This is the change that
actually fixes #8401.
|
|
|
|
|
|
|
|
|
|
This refines even further c24bcae8 (PR #924) and 6304c843:
- c24bcae8 fixed the order in the heuristic
- 6304c843 improved the order by preferring projections
There remained a dependency in the alphabetic order in selecting
unification candidates. The current commit fixes it.
We radically change the representation of the substitution to invert
by using a map indexed on the rank in the signature rather than on the
name of the variable.
More could be done to use numbers further, e.g. for representing
aliases.
Note that this has consequences on the test-suite (in
output/Notations.v) as some problems now infer a dependent return
clause.
|
|
|
|
|
|
|
|
|
|
|
|
It seems people don't always look at the test suite readme.
|
|
This allows for nicer formatting without having to deal with Make's
semantic whitespace.
|
|
As far as I know, this plugin is untested and barely maintained. I don't
think it has real use cases any more, so let's move it out from the repo
and see if somebody wants to take over and maintain it.
We also remove the documentation, which was telling our users to look at
ring to see an example of reification done using quote, when in fact it
wasn't using it anymore.
|
|
|
|
|
|
This concerns e.g. "?[id]", "?[?id]" or "?id" (in terms, not in
patterns), so that all names occurring in terms are consistently
interpreted as ltac names.
Moreover, with that, we can for instance do:
Ltac pick x := eexists ?[x].
Goal exists x, x = 0.
pick foo.
|
|
|
|
|
|
|
|
from compiles files
|
|
variables
|
|
Removing in passing two Local which are no-ops in practice.
|
|
The parts of pattern-matching compilation which generated names may
generate names which collided with names of the Ltac environment.
We fix it by avoiding the names of the Ltac environment.
|
|
The recursion names in fix and cofix were not renamed like other
binders were.
|
|
This module contains:
- the former ExtraEnv in pretyping
- a few functions to traverse binders in pretyping.ml and cases.ml
- the part of pretyping dealing with genarg interpretation
The dependency of pretyping in an interpretation of names as names of
variables of identifier is now hidden in GlobEnv (no more explicit
"lvar" management in pretyping.ml). Similarly for the interpretation
of names as terms and for the interpretation of tactics-in-terms.
We keep empty_lvar in Glob_ops for compatibility, even though it is a
bit isolated there.
|
|
One didn't normalize the bodies of fixpoints according to the universe
context, resulting in a type errors. Use EConstr.to_constr to ensure
universes are normalized instead of using EConstr.Unsafe.to_constr.
|
|
|
|
|
|
|
|
This fixes the fix 1522b989 to #7192.
The remaining Not_found after 1522b989 should have rung a bell that
something was still strange.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
then only parsing
|
|
with no binders
|
|
Fixes #8311
|
|
|
|
Notations were not initially designed to support independent parsing
and printing rules. Some redesign of this part of the code shall be
necessary at some time.
|
|
Numeral Notations are not well-supported inside functors. We now give a
proper error message rather than an anomaly when this occurs.
|
|
|
|
Thanks to Emilio and Pierre-Marie Pédrot for pointers.
|
|
Because that's the sane thing to do.
This will inevitably cause issues for projects which do not `Import
Coq.Strings.Ascii` before trying to use ascii notations.
We also move the syntax plugin for `int31` notations from `Cyclic31` to
`Int31`, so that users (like CompCert) who merely `Require Import
Coq.Numbers.Cyclic.Int31.Int31` get the `int31` numeral syntax. Since
`Cyclic31` `Export`s `Int31`, this should not cause any additional
incompatibilities.
|
|
Aliases of global references can now be used in numeral notations
|
|
Now we support using inductive constructors and section-local variables
as numeral notation printing and parsing functions.
I'm not sure that I got the econstr conversion right.
|
|
As per https://github.com/coq/coq/pull/8064#discussion_r209875616
I decided to make it a warning because it seems more flexible that way;
users to are flipping back and forth between option types and not option
types while designing won't have to update their `abstract after`
directives to do so, and users who don't want to allow this can make it an
actual error message.
|
