| Age | Commit message (Collapse) | Author |
|---|
|
|
|
`coe_source` and `coe_target` fields of type `cl_typ` have been added to
`coe_info_typ` so that it allows querying the classes from a `GlobRef.t` of a
coercion. The `coercion` record has also been replaced with `coe_info_typ`.
|
|
The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of
integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been
replaced with `cl_typ` and `ClTypMap` respectively.
|
|
Reviewed-by: Zimmi48
Ack-by: JasonGross
|
|
|
|
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: JasonGross
Reviewed-by: MSoegtropIMC
|
|
Reviewed-by: ppedrot
|
|
solve_constraints
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
Reviewed-by: ppedrot
Reviewed-by: ejgallego
|
|
|
|
|
|
By separating the libobject for create db and other hints we can unify
handling of local/superglobal.
|
|
ssreflect asks setoid rewrite to rewrite in goal
"forall_special_name_ : T, _other_name_"
Since this is a non dependent product, setoid rewrite converts that to
"impl T _other_name_" and must be taught to restore the special name
when unfolding impl.
|
|
Reviewed-by: Zimmi48
Ack-by: JasonGross
Ack-by: gares
Ack-by: LasseBlaauwbroek
Ack-by: silene
Ack-by: vbgl
|
|
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.
|
|
raised.
Reviewed-by: jfehrle
|
|
Reviewed-by: jfehrle
|
|
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
|
|
Now that they are well described on the website.
|
|
|
|
native_compute is called.
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
|
|
Reviewed-by: silene
Reviewed-by: gares
|
|
|
|
|
|
This was deprecated in 8.12
|
|
Reviewed-by: SkySkimmer
Reviewed-by: silene
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: proux01
|
|
This has been in the TODO queue for a long time, and indeed
I have recently seen some trouble with users passing two .v files to
Coq, which it isn't a) tested, b) supported.
Moreover, it doesn't even work correctly in 8.13 due to some other
changes in the toplevel related to auxiliary files.
(*) https://stackoverflow.com/questions/66261987/compiling-multiple-coq-files-does-not-work
|
|
Reviewed-by: gares
|
|
Reviewed-by: ejgallego
|
|
|
|
|
|
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.
|
|
Reviewed-by: ppedrot
|
|
caml_something_to_do.
Reviewed-by: gasche
Ack-by: ppedrot
Reviewed-by: xavierleroy
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
called (fix #13849).
The libraries are eventually linked in native_norm and native_conv_gen,
just before mk_norm_code and mk_conv_code are called.
This commit also renames call_linker as execute_library to better reflect
its role. It also makes link_library independent from it, since their
error handling are completely opposite.
|
|
Reviewed-by: gares
Ack-by: SkySkimmer
|
|
PR #13183 introduced quite a bit of duplicate code, we refactor it and
expose less internals on the way. That should make the API more
robust.
|
|
Reviewed-by: gares
Ack-by: herbelin
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer
Ack-by: ejgallego
|
