| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |\ |
|
| |\ \
| | |
| | |
| | | |
(clause "where" with implicit arguments)
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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`.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We improve one step further the heuristics to sort out if a variable
is a notation variable or a named variable.
This allows to support the following which was still failing.
Reserved Notation "# x" (at level 0).
Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I).
We rely here on the property that a binding variable of same name as a
notation variables is itself considered bound by the notation.
This becomes however to be a bit tricky for sorting out if the
variable has to be output to the glob file or not.
|
| |/ |
|
| |\
| |
| |
| | |
clause of an inductive definitions
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This allows e.g. the following to work:
Reserved Notation "* a" (at level 70).
Inductive P {n : nat} : nat -> Prop := c m : *m where "* m" := (P m).
We seize this opportunity to make main calls to Metasyntax to depend
on an arbitrary env rather than on Global.env.
Incidentally, this fixes a little coqdoc bug in classifying the
inductive type referred to in the "where" clause.
|
| |/
|
|
|
| |
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).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.
We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.
Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).
We also fix a regression in the test-suite:
Mixing laziness and effects is a well-known hell. Here, an exception
that was raised for mere control purpose was delayed and raised at a
later time as an anomaly. We make the offending function eager.
|
| |
|
|
| |
Use the functional interface understand_tcc instead.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Note that localisation cannot be perfect anyways, as in the following
example, where there is no way to highlight in the original input a
syntactically stand-alone subterm where the error occurs.
> Check forall (y:nat) (x:=0), y.
> ^^^^^^^^^^^^^^^^^^^^^^^^
Error: In environment
y : nat
The term "let x := 0 in y" has type "nat" which should be Set, Prop or Type.
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
This string contains the base-10 representation of the number (big endian)
Note that some inner parsing stuff still uses bigints, see egramcoq.ml
|
| |/ |
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
short econstr-cleaning of record.ml
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
a flag suspectingly renamed in a clearer way
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
As per https://github.com/coq/coq/pull/716#issuecomment-305140839
Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
A priori considered to be a good programming style.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This highlights that this is a binary mode changing the interpretation
of "?x" rather than additionally allowing patvar.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This module collects the functions of Nameops which are about Name.t
and somehow standardize or improve their name, resulting in particular
from discussions in working group.
Note the use of a dedicated exception rather than a failwith for
Nameops.Name.out.
Drawback of the approach: one needs to open Nameops, or to use long
prefix Nameops.Name.
|
| | | |/ / /
| |/| | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Also trying to reformulate the message, distinguishing between a
variable/parameter and its name.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We want to avoid capture in "Inductive I {A} := C : forall A, I".
But in "Record I {A} := { C : forall A, A }.", non recursivity ensures
that no clash will occur.
This fixes previous commit, with which it could possibly be merged.
|
| | | |/ /
| |/| |
| | | |
| | | |
| | | |
| | | | |
For instance, the following was failing to use the implicitness of n:
Inductive A (P:forall m {n}, n=m -> Prop) := C : P 0 eq_refl -> A P.
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This allows a better control on the name to give to an evar and, in
particular, to address the issue about naming produced by "epose
proof" in one of the comment of Zimmi48 at PR #248 (see file names.v).
Incidentally updating output of Show output test (evar numbers shifted).
|
| |/ /
| |
| |
| |
| |
| | |
Constrintern.pf_global returns a global_reference, not a constr,
adapt plugins accordingly, properly registering universes where
necessary.
|
| | |\ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
|
| |\ \ \ |
|
| | | | | |
|
| |\ \ \ \ |
|
| | | |\ \ \
| | |/ / /
| |/| | | |
|
| | |\ \ \ \
| | | |/ /
| | |/| | |
|
| | |\ \ \ \ |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
We seized this opportunity to factorize the code for interning `pat
with more general pre-existing code.
More precisely: There was already a function to compute the free
variables of a pattern. Commit c6d9d4fb rewrote an approximation of it
and #5222 hits cases non-treated by this function. We remove the
partially-defined redundant code and use instead the existing code
since intern_cases_pattern, already called, was already doing this
computation. (In doing so, we discover a bug in merging names in the
presence of nested "as" clauses, which we fix in previous
commit. Additionally, intern_local_pattern was misleadingly overkill
to simply mean a folding on Id.Set.add and we avoid the detour.
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
1969e10f25df0c913600099b7b98ea273a064017 introduced a check so a cast
in a pattern is not a fatal error.
We move this check to the internalization function, which is the
logical place to raise it, removing a bit boilerplate code.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
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`.
|
| | |/ / / / |
|
| | | |/ /
| |/| | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Following @gasche idea, and the original intention of #402, we switch
the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast`
which is private and record-based.
This provides significantly clearer code for the AST, and is robust
wrt attributes.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.
We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.
The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
|
Maxime Dénès
Emilio Jesus Gallego Arias
Hugo Herbelin
Pierre-Marie Pédrot
Pierre Letouzey
Guillaume Melquiond
Jason Gross
Matthieu Sozeau
Matej Košík
Gaetan Gilbert