coq/plugins/setoid_ring, branch master

{new,setoid_}ring -> ring

2020-10-02T11:23:30+00:00

I believe this renaming makes it easier for new contributors to discover
the code of `ring`.

Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.

2020-09-22T16:22:12+00:00

ring: generate fresh names for lemmas

2020-08-25T13:01:27+00:00

Fix #12889

UIP in SProp

2020-07-01T11:06:22+00:00

Moving the remaining Refiner functions to Tacmach.

2020-06-29T13:17:20+00:00

Remove useless try-with clauses in newring.

2020-05-12T10:58:35+00:00

This is already protected by then enter block.

[declare] [tactics] Move declare to `vernac`

2020-04-21T06:39:12+00:00

This PR moves `Declare` to `vernac` which will hopefully allow to
unify it with `DeclareDef` and avoid exposing entry internals.

There are many tradeoffs to be made as interface and placement of
tactics is far from clear; I've tried to reach a minimally invasive
compromise:

- moved leminv to `ltac_plugin`; this is unused in the core codebase
  and IMO for now it is the best place
- hook added for abstract; this should be cleaned up later
- hook added for scheme declaration; this should be cleaned up later
- separation of hints vernacular and "tactic" part should be also done
  later, for now I've introduced a `declareUctx` module to avoid being
  invasive there.

In particular this last point strongly suggest that for now, the best
place for `Class_tactics` would be also in `ltac`, but I've avoided
that for now too.

This partially supersedes #10951 for now and helps with #11492 .

[dune] [stdlib] Build the standard library natively with Dune.

2020-04-11T21:45:18+00:00

This completes a pure Dune bootstrap of Coq.

There is still the question if we should modify `coqdep` so it does
output a dependency on `Init.Prelude.vo` in certain cases.

TODO: We still double-add `theories` and `plugins` [in coqinit and in
Dune], this should be easy to clean up.

Setting `libs_init_load_path` does give a correct build indeed;
however we still must call this for compatibility?

Update headers in the whole code base.

2020-03-18T11:15:43+00:00

Add headers to a few files which were missing them.

[build] Consolidate stdlib's .v files under a single directory.

2020-02-13T20:12:03+00:00

Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.

This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.

We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.

Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.

This could also imply a performance gain as we now effectively
traverse less directories when locating a library.

See also discussion in #10003