| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: JasonGross
Reviewed-by: MSoegtropIMC
|
|
|
|
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.
|
|
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.
|
|
Reviewed-by: silene
Reviewed-by: gares
|
|
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
|
|
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: silene
Ack-by: SkySkimmer
|
|
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: vbgl
|
|
Closes #13794
|
|
Warnings are handled as injection commands, interleaved with options
and requires. Native compiler impacts require, so we must convert
"yes" to "no" before handling injections. As such the semantic
handling of the native command line argument must be separated from
the emission of the warning message, which this PR implements.
Fix #13819
In principle the other 2 cwarning in coqargs
(deprecated spropcumul and inputstate) should be moved to injections
too, but since they're deprecated I can't be bothered.
|
|
Also added a generic way of temporarily disabling a warning.
Also added try_finalize un lib/utils.ml.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
Fixes #13755 .
|
|
|
|
Reviewed-by: gares
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
|
|
inductive definitions.
Reviewed-by: SkySkimmer
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
pattern
Reviewed-by: ppedrot
|
|
Ack-by: Zimmi48
Ack-by: gares
Reviewed-by: ppedrot
|
|
|
|
We build earlier the final expected name at the end of a sequence of
"%" introduction patterns.
|
|
We deprecate unspecified locality as was done for Hint.
Close #13724
|
|
Also works for simpl.
|
|
|
|
|
|
|
|
The arity of a destructuring let in a pattern is allowed to be shorter than
the case term node it actually matches. This is an unexpected side-effect
of the legacy expanded representation of cases that happens to be relied
upon in the wild, as evidenced by the CI failures from #13723.
|
|
This returns to the previous behaviour of Implicit Type forgetting
universes.
`Implicit Type T : Type@{u}.` may be confusing as it is equivalent to
`: Type`, but until we have a better idea of what to do with anonymous
types I see no other solution, especially in the short term to fix the
bug.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
|
|
at ..." instead)
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: vbgl
|
|
|
|
|
|
Destruct has changed semantics, but I'd like to see how CI fares so far.
|
|
Fixes #3166.
|
|
(use "with ... at ..." instead)
|
|
|
|
let-bindings.
|
|
|
|
This is extracted from #13563.
|
