diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/SProp.md | 41 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 4 | ||||
| -rw-r--r-- | dev/doc/changes.md | 8 |
3 files changed, 51 insertions, 2 deletions
diff --git a/dev/doc/SProp.md b/dev/doc/SProp.md new file mode 100644 index 0000000000..f263dbb867 --- /dev/null +++ b/dev/doc/SProp.md @@ -0,0 +1,41 @@ +# Notes on SProp + +(ml API side, see refman for user side) + +## Relevance + +All kernel binders (`Prod`/`Lambda`/`LetIn`/`Context` elements) are +now annotated with a value in `type Sorts.relevance = Relevant | +Irrelevant`. It should verify that the binder's type lives in `SProp` +iff the annotation is `Irrelevant`. + +As a plugin you can generally just use `Relevant` everywhere, the +kernel will fix it if needed when it checks the terms you produce. The +only issue is that if you generate `Relevant` when it should have been +`Irrelevant` you won't be able to use proof irrelevance on that +variable until the kernel fixes it. See refman for examples as Coq +also uses `Relevant` incorrectly in some places. + +This annotation is done by transforming the binder name `'a` into a +`'a Context.binder_annot = { binder_name : 'a; binder_relevance : +Sorts.relevance }`, eg `Prod of Name.t * types * types` becomes `Prod +of Name.t Context.binder_annot * types * types`. + +If you just carry binder names around without looking at them no +change is needed, eg if you have `match foo with Lambda (x, a, b) -> +Prod (x, a, type_of (push_rel (LocalAssum (x,a)) env) b)`. Otherwise +see `context.mli` for a few combinators on the `binder_annot` type. + +When making `Relevant` annotations you can use some convenience +functions from `Context` (eg `annotR x = make_annot x Relevant`), also +`mkArrowR` from `Constr`/`EConstr` which has the signature of the old +`mkArrow`. + +You can enable the debug warning `bad-relevance` to help find places +where you generate incorrect annotations. + +Relevance can be inferred from a well-typed term using functions in +`Retypeops` (for `Constr`) and `Retyping` (for `EConstr`). For `x` a +term, note the difference between its relevance as a term (is `x : +(_ : SProp)`) and as a type (is `x : SProp`), there are functions for +both kinds. diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index a31ab1c511..b1bfac8cc9 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -126,9 +126,9 @@ script again] This will be fixed in the future. ## Dropping from coqtop: -The following sequence is recommended: +After doing `make -f Makefile.dune voboot`, the following commands should work: ``` -dune exec coqtop.byte +dune exec dev/shim/coqbyte-prelude > Drop. # #directory "dev";; # #use "include_dune";; diff --git a/dev/doc/changes.md b/dev/doc/changes.md index e7d4b605c7..d515ec30e8 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -12,6 +12,8 @@ ### ML API +SProp was added, see <SProp.md> + General deprecation - All functions marked [@@ocaml.deprecated] in 8.8 have been @@ -72,6 +74,12 @@ Libobject * `Libobject.superglobal_object` * `Libobject.superglobal_object_nodischarge` +Implicit Arguments + +- `Impargs.declare_manual_implicits` is restricted to only support declaration + of implicit binders at constant declaration time. `Impargs.set_implicits` should + be used for redeclaration of implicit arguments. + ## Changes between Coq 8.8 and Coq 8.9 ### ML API |