coq/tools/coqdoc, branch master The formal proof system Merge PR #14038: [dune] [coqdoc] Install coqdoc.sty also in share/texmf 2021-04-12T14:21:34+00:00 coqbot-app[bot] 2021-04-12T14:21:34+00:00 bba57138fcb0badf307fb00b97d73b4933e3022b Reviewed-by: Zimmi48 
Reviewed-by: Zimmi48
Remove the omega tactic and related options 2021-04-03T01:52:59+00:00 Jim Fehrle 2021-01-11T22:47:13+00:00 d3a51ac24244f586dfeff1a93b68cb084370534e 






[dune] [coqdoc] Install coqdoc.sty also in share/texmf
2021-03-31T17:00:20+00:00

Emilio Jesus Gallego Arias

2021-03-31T17:00:20+00:00

3d40b663fbefecbeb5b23dd9656c5342269c284a












[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.







Get rid of the compilation date from the binaries to make them more stable.
2021-02-16T08:02:37+00:00

Guillaume Melquiond

2021-02-16T08:02:37+00:00

31e205ae752c5189143ef9ce87a3536db0cdeb62

Contrarily to the comments, Coq_config.date was not the "release date" but
just another "compile date".





Contrarily to the comments, Coq_config.date was not the "release date" but
just another "compile date".







Remove the SearchHead command
2021-01-25T18:26:13+00:00

Jim Fehrle

2021-01-19T19:55:49+00:00

3d46bed76e656d6a0e4d87320e4d0fd67d1211c2












Avoid using "subgoals" in the UI, it means the same as "goals"
2021-01-13T23:24:23+00:00

Jim Fehrle

2020-12-17T23:04:36+00:00

3da2dbe9728ae7f5b1860a8e3a6c458e6d976f84












Fix broken HTML rendering of inference rules (fix #12783).
2020-12-28T10:26:54+00:00

Guillaume Melquiond

2020-12-28T09:29:34+00:00

aed648afd2cf8b09d67fb39c9672b71166089395












Coqdoc: we move a newline at a better place.
2020-11-14T21:55:47+00:00

Hugo Herbelin

2020-11-05T15:17:37+00:00

696df507b58800a7a6b52741fd4ed859aff7b1c3

This does not affect the rendering but gives better structured
html/tex files.





This does not affect the rendering but gives better structured
html/tex files.







Addressing #13304: how to verbatim an expression mentioning >>.
2020-11-14T21:55:47+00:00

Hugo Herbelin

2020-11-05T12:08:14+00:00

7923bb570cd493aff31ac1c94f9e03ff4efd465f

We clarify that there are two kinds of verbatim: inline and block.

We add a test testing verbatim and others.

Co-authored-by: Xia Li-yao <Lysxia@users.noreply.github.com>





We clarify that there are two kinds of verbatim: inline and block.

We add a test testing verbatim and others.

Co-authored-by: Xia Li-yao <Lysxia@users.noreply.github.com>