| Age | Commit message (Collapse) | Author |
|---|
|
cache_function is called from add_leaf and after discharging sections,
but default_object is section local.
|
|
Reviewed-by: SkySkimmer
Ack-by: jfehrle
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
We introduce a new package structure for Coq:
- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`
This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.
The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.
Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.
There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.
This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.
IMHO the plan should work fine.
|
|
This was deprecated in 8.12
|
|
Signed primitive integers defined on top of the existing unsigned ones
with two's complement.
The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.
Additions to the kernel:
les (signed <=), lts (signed <), compares (signed compare),
divs (signed division), rems (signed remainder),
asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)
The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).
A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
This was raising a Not_found exception due to the unknown scope.
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
|
|
|
|
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
|
|
|
|
notations.
Reviewed-by: jfehrle
Reviewed-by: proux01
Ack-by: Zimmi48
Ack-by: SkySkimmer
|
|
Reviewed-by: ppedrot
Reviewed-by: proux01
|
|
Namely, WrongNumargInductive and WrongNumargConstructor.
|
|
|
|
|
|
Also includes a try/let commutation for uniformity.
|
|
Also includes some fine-tuning of error messages.
|
|
|
|
There are calls now in intern_impargs and CAppExpl.
This seems clearer and eventually allow to factorize code between term
and pattern interning.
|
|
We also simplify the whole process of interpretation of cases pattern
on the way.
|
|
|
|
notation.
|
|
|
|
|
|
- float and array values are now supported for printing and parsing in custom notations (and in notations defined using the ocaml API)
- the three constants bound to the primitive float, int and array type are now allowed anywhere inside a term to print, to handle them similar to `real` type constructors
- Grants #13484: String notations for primitive arrays
- Fixes #13517: String notation printing fails with primitive integers inside lists
|
|
|
|
This allows proper treatment in notations, ie fixes #13303
The "glob" representation of universes (what pretyping sees) contains
only fully interpreted (kernel) universes and unbound universe
ids (for non Strict Universe Declaration).
This means universes need to be understood at intern time, so intern
now has a new "universe binders" argument. We cannot avoid this due to
the following example:
~~~coq
Module Import M. Universe i. End M.
Definition foo@{i} := Type@{i}.
~~~
When interning `Type@{i}` we need to know that `i` is locally bound to
avoid interning it as `M.i`.
Extern has a symmetrical problem:
~~~coq
Module Import M. Universe i. End M.
Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
Print foo. (* must not print Type@{i} -> Type@{i} *)
~~~
(Polymorphic as otherwise the local `i` will be called `foo.i`)
Therefore extern also takes a universe binders argument.
Note that the current implementation actually replaces local universes
with names at detype type. (Asymmetrical to pretyping which only gets
names in glob terms for dynamically declared univs, although it's
capable of understanding bound univs too)
As such extern only really needs the domain of the universe
binders (ie the set of bound universe ids), we just arbitrarily pass
the whole universe binders to avoid putting `Id.Map.domain` at every
entry point.
Note that if we want to change so that detyping does not name locally
bound univs we would need to pass the reverse universe binders (map
from levels to ids, contained in the ustate ie in the evar map) to
extern.
|
|
coercion not being used
Reviewed-by: ejgallego
|
|
notations.
Reviewed-by: jfehrle
Reviewed-by: gares
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
sense
Reviewed-by: Zimmi48
|
|
We use a deprecation phase where:
- "ident" means "name" (as it used to mean), except in custom coercion
entries where it already meant "ident".
- "ident" will be made again available (outside situation of
coercions) to mean "ident" at the end of deprecation phase.
Also renaming "as ident" into "as name".
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
|
|
In #11172, an "=" on the number of arguments of an applied coercion
had become a ">" on the number of arguments of the coercion. It should
have been a ">=". The rest of changes in constrextern.ml is "cosmetic".
Note that in #11172, in the case of a coercion to funclass, the
definition of number of arguments of an applied coercion had moved
from including the extra arguments of the coercion to funclass to
exactly the nomber of arguments of the coercion (excluding the extra
arguments). This was necessary to take into account that several
coercions can be nested, at least of those involving a coercion to
funclass.
Incidentally, we create a dedicated output file for notations and
coercions.
|
|
This avoids relying on fragile invariants.
|
|
We at least support a cast at the top of patterns in notations.
|
|
We introduce a class of open binders which includes "x", "x:t", "'pat"
and a class of closed binders which includes "x", "(x:t)", "'pat".
|
|
|
|
between variable and non-qualified global references
Reviewed-by: ejgallego
Ack-by: maximedenes
Ack-by: gares
|
|
|
|
binder
Reviewed-by: herbelin
|
|
then by last imported
Reviewed-by: Zimmi48
Ack-by: RalfJung
Ack-by: gares
|
|
This allows e.g. to support a notation of the form "x <== y <== z <= t"
standing for "x <= y /\ y <= z /\ z <= t".
|
|
Reviewed-by: herbelin
|
|
|
|
This relies on finer-than partial order check with. In particular:
- number and order of notation metavariables does not matter
- take care of recursive patterns inclusion
|
|
Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: ppedrot
|
|
The name bound in binders were not checked up to alpha-equivalence,
nor were the names binding the recursive patterns.
|
