| Age | Commit message (Collapse) | Author |
|---|
|
* Borrow ideas from the Setoid refman documentation:
https://coq.inria.fr/refman/addendum/generalized-rewriting.html#first-class-setoids-and-morphisms
* Introduce a relation with the following signature:
[Rel : forall (m n : nat) (s : Setoid m n), car s -> car s -> Prop]
|
|
Changes:
* Add ssrclasses.v that redefines [Reflexive] and [iff_Reflexive];
* Add ssrsetoid.v that links
[ssrclasses.Reflexive] and [RelationClasses.Reflexive];
* Add [Require Coq.ssr.ssrsetoid] in Setoid.v;
* Update ssrfwd.ml accordingly, using a helper file ssrclasses.ml that
ports some non-exported material from rewrite.ml;
* Some upside in passing: ssrfwd.ml no more depends on Ltac_plugin;
* Update doc and tests as well.
Summary:
* We can now use the under tactic in two flavors:
- with the [eq] or [iff] relations: [Require Import ssreflect.]
- or a [RewriteRelation]: [Require Import ssreflect. Require Setoid.]
(while [ssreflect] does not require [RelationClasses] nor [Setoid],
and conversely [Setoid] does not require [ssreflect]).
* The file ssrsetoid.v could be skipped when porting under to stdlib2.
|
|
* Add an extra test with an Equivalence.
* Update the doc accordingly.
|
|
All the implementations now return (0, 0) when the dividend is so large
that the quotient would overflow.
|
|
|
|
The documentation states:
- Norm means the term is fully normalized and cannot create a redex
when substituted
- Cstr means the term is in head normal form and that it can
create a redex when substituted (i.e. constructor, fix, lambda)
|
|
rewrite
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Ack-by: ejgallego
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: mattam82
|
|
Fixes #10300 and #10285.
|
|
The issue could be reproduced by doing "dune build
test-suite/misc/universes/all_stdlib.v" (from a clean build) which
would error 127 with no message.
- only redirect stdout so that in the future we will see error
messages
- put the script as a dependency (I guess it sometime succeeded when
copying the deps for the test suite happened before running it)
|
|
|
|
This is deemed to be more natural as most of the uses will follow this
structure.
|
|
The previous implementation allowed to dynamically decide whether a section
would be monomorphic or polymorphic at the first definition of a variable
or a constraint. Instead of relying on this delayed decision, we set the
universe polymorphic property directly at the time of the section definition.
|
|
Reviewed-by: SkySkimmer
Ack-by: herbelin
|
|
We should have this in the check target, but meanwhile we have to do
manual housekeeping here.
|
|
new one
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: herbelin
Ack-by: jfehrle
|
|
Reviewed-by: ejgallego
|
|
It prints a goal given its internal goal id and the Stm state id.
|
|
This looks more principled, and doesn't require as much tinkering with
the typing implementation.
|
|
|
|
Ack-by: SkySkimmer
Ack-by: mattam82
Reviewed-by: ppedrot
|
|
with coqtop
Reviewed-by: gares
Ack-by: jfehrle
|
|
- fix the printers themselves after discharge was moved to the kernel
- change the test to make it more robust
In addition to checking that there is no "Error|Unbound" in the
output, ensure that the "go" function at the end of base_include
is defined. If there are any errors in base_include it won't be defined.
This makes us find out that the test was silently failing in all CI
jobs except trunk+make. It failed to find the "include" file and so
failed with "could not find file include.", which we didn't detect.
To fix this:
- change automatically included paths in Coqinit.init_ocaml_path to be
based on coqlib instead of coqroot. This way top_printers.ml and
base_include can find the compiled ml objects.
- fix for dune: adapt the script to use include_dune when INSIDE_DUNE,
add dependencies to test-suite/dune.
The dependencies should be calculated automatically once Dune has
better support for debug, or we implement proper support for test
printers.
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
|
This allows to desynchronize the kernel-facing API from the proof-facing one.
|
|
(fix #10350)
Ack-by: gares
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
|
|
local fix/cofix (#10197)
Reviewed-by: maximedenes
|
|
|
|
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: maximedenes
|
|
definitions
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ggonthier
Reviewed-by: herbelin
|
|
This replaces the mismatched context error, which occurred when
Instance := {} was used with strictly more fields than declared.
Since we later check that field names match those declared for the
instance, now that we reject duplicates we know that there are no
extra fields.
|
|
Reviewed-by: aspiwack
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
Formerly, knowing if a declaration was to be discharged, to be global
but invisible at import, or to be global but visible at import was
obtained by combining the parser-level information (i.e. use of
Variable/Hypothesis/Let vs use of Axiom/Parameter/Definition/..., use
of Local vs Global) with the result of testing whether there were open
sections.
We change the meaning of the Discharge flag: it does not tell anymore
that it was syntactically a Variable/Hypothesis/Let, but tells the
expected semantics of the declaration (issuing a warning in the
parser-to-interpreter step if the semantics is not the one suggested
by the syntax). In particular, the interpretation/command engine
becomes independent of the parser.
The new "semantic" type is:
type import_status = ImportDefaultBehavior | ImportNeedQualified
type locality = Discharge | Global of import_status
In the process, we found a couple of inconsistencies in the treatment
of the locality status. See bug #8722 and test file LocalDefinition.v.
|
|
I don't know what goal_selector.v was supposed to test but CI says
nobody relied on it.
|
|
interpretation scopes
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Ack-by: vbgl
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
|
|
Type's argument
Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
|
|
Reviewed-by: gares
|
