| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
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.
|
|
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.
|
|
|
|
|
|
Fixes #8311
|
|
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.
|
|
Also make `Check S` no longer anomaly
Add a couple more test cases for numeral notations
Also add another possibly-confusing error message to the doc.
Respond to Hugo's doc request with Zimmi48's suggestion
From https://github.com/coq/coq/pull/8064/files#r204191608
|
|
Some of this code is cargo-culted or kludged to work.
As I understand it, the situation is as follows:
There are two sorts of use-cases that need to be supported:
1. A plugin registers an OCaml function as a numeral interpreter. In
this case, the function registration must be synchronized with the
document state, but the functions should not be marshelled / stored
in the .vo.
2. A vernacular registers a Gallina function as a numeral interpreter.
In this case, the registration must be synchronized, and the function
should be marshelled / stored in the .vo.
In case (1), we can compare functions by pointer equality, and we should
be able to rely on globally unique keys, even across backtracking.
In case (2), we cannot compare functions by pointer equality (because
they must be regenerated on unmarshelling when `Require`ing a .vo file),
and we also cannot rely on any sort of unique key being both unique and
persistent across files.
The solution we use here is that we ask clients to provide "unique"
keys, and that clients tell us whether or not to overwrite existing
registered functions, i.e., to tell us whether or not we should expect
interpreter functions to be globally unique under pointer equality. For
plugins, a simple string suffices, as long as the string does not clash
between different plugins. In the case of vernacular-registered
functions, use marshell a description of all of the data used to
generate the function, and use that string as a unique key which is
expected to persist across files. Because we cannot rely on
function-pointer uniqueness here, we tell the
interpretation-registration to allow overwriting.
----
Some of this code is response to comments on the PR
----
Some code is to fix an issue that bignums revealed:
Both Int31 and bignums registered numeral notations in int31_scope. We
now prepend a globally unique identifier when registering numeral
notations from OCaml plugins. This is permissible because we don't
store the uid information for such notations in .vo files (assuming I'm
understanding the code correctly).
|
|
|
|
|
|
Also prevents to use an entry name already defined.
|
|
This is in preparation of changes in level_eq, to check that the
semantics is preserved.
|
|
|
|
As stated in the manual, the fourier tactic is subsumed by lra.
|
|
We make it possible to deprecate tactics defined by `Ltac`, `Tactic
Notation` or ML.
For the first two variants, we anticipate the syntax of attributes:
`#[deprecated(since = "XX", note = "YY")]`
In ML, the syntax is:
```
let reflexivity_depr =
let open CWarnings in
{ since = "8.5"; note = "Use admit instead." }
TACTIC EXTEND reflexivity DEPRECATED reflexivity_depr
[ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
END
```
A warning is shown at the point where the tactic is used (either
a direct call or when defining another tactic):
Tactic `foo` is deprecated since XX. YY
YY is typically meant to be "Use bar instead.".
|
|
|
|
|
|
This gives user control on the transparent state of a hint db. Can
override defaults more easily (report by J. H. Jourdan).
For "core", declare that variables can be unfolded, but no constants
(ensures compatibility with previous auto which allowed conv on closed
terms)
Document Hint Variables
|
|
|
|
|
|
|
|
|
|
This ensures that computations are shared as much as possible, mimicking
the "positive" records computational behavior if possible.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We add a [SelectAlreadyFocused] constructor to [goal_selector] (read
"!") which causes a failure when there's not exactly 1 goal and
otherwise is a noop.
Then [Set Default Goal Selector "!".] puts us in "strict focusing"
mode where we can only run tactics if we have only one goal or use a
selector.
Closes #6689.
|
|
|
|
|
|
LTAC's `fix` and `cofix` do require access to the proof object inside
the tactic monad when used without a name. This is a bit inconvenient
as we aim to make the handling of the proof object purely functional.
Alternatives have been discussed in #7196, and it seems that
deprecating the nameless forms may have the best cost/benefit ratio,
so opening this PR for discussion.
See also #6171.
|
|
We take into account all future ipats, not just the ones in
the current branch
|
|
|
|
|
|
|
|
There is a code to turn constants denoting projections into proper
primitive projections, but it did not drop parameters.
The code seems anyway redundant with an "expand_projections" which is
already present in Cctac.decompose_term. After removal of this code,
the two calls to congruence added to cc.v work.
|
|
We expected `nparams + nrealargs + consnrealargs` but the `nrealargs`
should not be there. This breaks cumulativity of constructors for any
inductive with indices (so records still work, explaining why the test
case in #6747 works).
|
|
|
|
In Reductionops.infer_conv we did not have enough information to
properly try to unify irrelevant universes. This requires changing the
Reduction.universe_compare type a bit.
|
