| 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.
|
|
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.
|
|
|
|
|
|
from compiles files
|
|
Removing in passing two Local which are no-ops in practice.
|
|
The recursion names in fix and cofix were not renamed like other
binders were.
|
|
This fixes the fix 1522b989 to #7192.
The remaining Not_found after 1522b989 should have rung a bell that
something was still strange.
|
|
|
|
|
|
- New command "Declare Custom Entry bar".
- Entries can have levels.
- Printing is done using a notion of coercion between grammar
entries. This typically corresponds to rules of the form
'Notation "[ x ]" := x (x custom myconstr).' but also
'Notation "{ x }" := x (in custom myconstr, x constr).'.
- Rules declaring idents such as 'Notation "x" := x (in custom myconstr, x ident).'
are natively recognized.
- Rules declaring globals such as 'Notation "x" := x (in custom myconstr, x global).'
are natively recognized.
Incidentally merging ETConstr and ETConstrAsBinder.
Noticed in passing that parsing binder as custom was not done as in
constr.
Probably some fine-tuning still to do (priority of notations,
interactions between scopes and entries, ...). To be tested live
further.
|
|
Print the expected and actual types for the option value (which is one
of bool, int, or string).
|
|
pattern (closes #7777)
|
|
This is particularly useful when the pattern is part of a disjunction.
Maybe this could be improved though, not mentioning the pattern when
there is no disjunction, but that would be more work.
|
|
No reason not to collapse inner applications with explicit arguments.
This is compatible with the ad hoc encoding of @f as GApp(f,[])/NApp(f,[]).
|
|
While we were adding a new field into `QuestionMark`, we
decided to go ahead and refactor the constructor to hold
an actual record. This record now holds the name, obligations, and
whether the evar represents a missing record field.
This is used to provide better error messages on missing record
fields.
|
|
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.".
|
|
In some cases, Format's inner boxes inside an outer box act as break
hints, even though there are already "better" break hints in the outer
box.
We work around this "feature" by not inserting a box around the
default printing rule for a notation if there is no effective break
points in the box.
See https://caml.inria.fr/mantis/view.php?id=7804 for the related
OCaml discussion.
|
|
of submodules.
|
|
|
|
Using a formulation which makes it is clear that no renaming has been
done. See discussion at issue #2987.
|
|
|
|
|
|
This was introduced between v8.5 and v8.6 (presumably 63f3ca8).
|
|
The five phases are command line interpretation, initialization,
prelude loading, rcfile loading, and sentence interpretation (only the
two latters are located).
We then parameterize the feedback handler with the given execution
phase, so as to possibly annotate the message with information
pertaining to the phase.
|
|
looking for a notation for a nested pattern
|
|
|
|
We fix it by looking manually for the implementation at each level of
nesting rather than using the signature for the n first levels and
looking for the implementation only in the n+1-th level.
|
|
|
|
|
|
|
|
Constrextern.explicitize expected that if implicits were declared they
would be declared at least up to the principal argument of the
projection, but Context/discharge of implicits does not preserve this.
Note the anomaly only happens with primitive projections DISABLED in
recent Coqs (>=8.8).
Implicit argument experts may consider whether ensuring enough
implicits are declared would be better.
|
|
|
|
For instance, error in "Goal forall a f, f a = 0" is now located.
|
|
notation to use among several of them"
This reverts commit 9cac9db6446b31294d2413d920db0eaa6dd5d8a6, reversing
changes made to 2f679ec5235257c9fd106c26c15049e04523a307.
|
|
|
|
|
|
|
|
Following up on #6791, we remove support refolding in reduction.
We also update a test case that was not properly understood, see the
discussion in #6895.
|
|
Since 4eb6d29d1ca7e0cc28d59d19a50adb83f7b30a2a universe binders were
declared twice for all records.
Since 4fcf1fa32ff395d6bd5f6ce4803eee18173c4d36 this causes an
observable error for monomorphic records.
|
|
|
|
Fix new deprecation warnings in the standard library.
|
|
We test the 3 possible scenarios. A more complete test would also
involved fake_ide.
c.f. #6793
|
|
infinite eta-expansion)
|
|
|
|
More precisely when matching
"f t" with "(fun ?x => .. ((fun ?x' => ?y) ?z') ..) ?z"
do not allow expansion of f since otherwise, we recursively have to
match "f t" with the same pattern.
|
|
Also changed the API of pr_subgoals now using labels.
Also removed a trailing space in printing existentials.
|
|
There is more churn than there should be because SearchPattern uses a
non-local sorting algorithm; the comparison function considers many
constants equal in priority and leaves it up to the heap structure to
break ties, which seems wrong. This has been reported as
[bug #5573](https://coq.inria.fr/bugs/show_bug.cgi?id=5573).
|
|
Concretely, we bypass the following limitation: The notation
"{ ' pat | P }" broke the parsing of expressions of the form
"{ forall x, P } + { Q }". Indeed the latter works thanks to a
tolerance of Camlp5 in parsing "forall x, P" at level 200 while the
rule asks to actually parse the interior of "{ ... }" at level 99 (the
reason for 99 is to be below the rule for "M : T" which is at level
100, so that "{ x : A | P }" does not see "x : A" as a cast). Adding
an extra "'"; pat = pattern in parallel to c = constr LEVEL "99" broke
the tolerance for constr at level 200.
We fix this by adding an ad hoc rule for "{ binder_constr }" in the
native grammar (g_constr.ml4).
Actually, this is inconsistent with having a rule for "{ constr at level 99 }"
in Notations.v. We should have both rules in Notations.v or both rules
hard-wired in the native grammar. But I still don't know what is the best
decision to take, so leaving as it at the current time.
Advantages of hard-wiring both rules in g_constr.ml4: a bit simpler in
metasyntax.ml (no need to ensure that the rule exist). Disadvantages:
if one wants a different initial state without the business needing
the "{ }" for sumbool, sumor, sig, sigT, one still have the rules
there.
Advantages of having them in Notations.v: more modular, we can change
the initial state. Disadvantages: one would need a new kind of
modifier, something like "x at level 99 || binder_constr", with all
the difficulty to find a nice, intuitive, name for "binder_constr",
and the difficulty of understanding if there is a generality to this
"||" disjunction operator, and whether it should be documented or not.
|
|
|
