coq/doc/plugin_tutorial/tuto3/src, branch master The formal proof system [build] Split stdlib to it's own opam package. 2021-03-03T15:06:14+00:00 Emilio Jesus Gallego Arias 2020-06-22T15:52:18+00:00 ab98d847d237af3cd0e46edef42218be65cfc98f 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. 
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.
[dune] Migrate static Dune files to Dune 1.10 2019-08-24T01:15:23+00:00 Emilio Jesus Gallego Arias 2019-08-24T01:02:19+00:00 a5b7ca5eadc5cf1c2e431ea8b540006ff063e5b8 This improves error reporting. Addendum to #10515 
This improves error reporting. Addendum to #10515
Update tutorial plugin to use sigma, in keeping with doc recommendations 2019-06-03T13:41:22+00:00 Talia Ringer 2019-06-03T13:41:22+00:00 a3fbe76736340e964917e6fcb9899735adb75eaf 






Fixing typos - Part 1
2019-05-21T21:07:55+00:00

JPR

2019-05-21T21:07:55+00:00

e6322e23958a937fa01960f8ce320717b9863253












Add relevance marks on binders.
2019-03-14T12:27:38+00:00

Gaëtan Gilbert

2017-10-31T16:04:02+00:00

23f84f37c674a07e925925b7e0d50d7ee8414093

Kernel should be mostly correct, higher levels do random stuff at
times.





Kernel should be mostly correct, higher levels do random stuff at
times.







plugin_tutorial: ignore Coqlib.find_reference deprecation warning.
2019-01-08T15:41:11+00:00

Gaëtan Gilbert

2019-01-07T13:09:58+00:00

8801a2304d54e687dafc8614af38f69ada2cbee1

Not sure what the right solution is here, but we can improve after the merge.





Not sure what the right solution is here, but we can improve after the merge.







Add 'doc/plugin_tutorial/' from commit '168a13dab1c9987f592994150997e692d4d7e40b'
2019-01-08T15:41:01+00:00

Gaëtan Gilbert

2019-01-07T12:24:14+00:00

fde557d9e92d2ddd3c79d8a620f2cb33ce64a49f

git-subtree-dir: doc/plugin_tutorial
git-subtree-mainline: 8c040974facb733682d24c488dc89941671f4ab7
git-subtree-split: 168a13dab1c9987f592994150997e692d4d7e40b





git-subtree-dir: doc/plugin_tutorial
git-subtree-mainline: 8c040974facb733682d24c488dc89941671f4ab7
git-subtree-split: 168a13dab1c9987f592994150997e692d4d7e40b