coq/doc/tools/docgram, branch master The formal proof system Merge PR #13965: [abbreviation] user syntax to set interp scope of argument 2021-04-23T14:33:27+00:00 Pierre-Marie Pédrot 2021-04-23T14:33:27+00:00 a0c3ebf4a6357a5140b98b4b40c71133c53d802e Ack-by: JasonGross Reviewed-by: herbelin Reviewed-by: jashug Reviewed-by: jfehrle Reviewed-by: ppedrot 
Ack-by: JasonGross
Reviewed-by: herbelin
Reviewed-by: jashug
Reviewed-by: jfehrle
Reviewed-by: ppedrot
Merge PR #13911: Remove the :> type cast? 2021-04-21T14:58:51+00:00 coqbot-app[bot] 2021-04-21T14:58:51+00:00 f9996cdaf0b6aee12c5b71432b1edb90dffb569a Reviewed-by: mattam82 Ack-by: Zimmi48 
Reviewed-by: mattam82
Ack-by: Zimmi48
Remove omega from doc_grammar files. 2021-04-12T14:38:55+00:00 Théo Zimmermann 2021-04-12T14:38:50+00:00 09fb4762de8b2dc256a43d6a931d5a479b98cd26 






[abbreviation] allow the user to set arguments scope
2021-04-07T17:59:46+00:00

Enrico Tassi

2021-03-19T13:29:07+00:00

d3963fc6b6dad5a0cf79815f31b2035ca8b3de25












Remove the omega tactic and related options
2021-04-03T01:52:59+00:00

Jim Fehrle

2021-01-11T22:47:13+00:00

d3a51ac24244f586dfeff1a93b68cb084370534e












Remove the :> type cast
2021-03-30T16:51:56+00:00

Jim Fehrle

2021-03-07T18:15:11+00:00

eeb142f3c69d2467fbadd7dd1470ac1606b2e5bf












Regenerate the Ltac2 syntax for documentation.
2021-03-10T11:20:27+00:00

Pierre-Marie Pédrot

2021-03-10T11:17:32+00:00

aba594ca194390bb00f8ef60ef8a5eef6694fc07












Merge PR #13707: Convert 2nd part of rewriting chapter to prodn
2021-03-08T20:22:04+00:00

coqbot-app[bot]

2021-03-08T20:22:04+00:00

b55216ab3509f48e45aac035f1b799529d068f51

Reviewed-by: Zimmi48
Ack-by: JasonGross





Reviewed-by: Zimmi48
Ack-by: JasonGross







Convert 2nd part of rewriting chapter to prodn
2021-03-08T19:48:20+00:00

Jim Fehrle

2020-09-13T03:54:22+00:00

0d33024ff79c38d52fde49e23d0e45d9c22eefbe












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