coq/dev/base_include, branch master

[recordops] complete API rewrite; the module is now called [structures]

2021-03-26T14:19:19+00:00

Replace cl_index with cl_typ in coercionops.ml

2021-03-09T09:10:23+00:00

The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of
integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been
replaced with `cl_typ` and `ClTypMap` respectively.

[sysinit] new component for system initialization

2021-01-27T08:45:49+00:00

This component holds the code for initializing Coq:
- parsing arguments not specific to the toplevel
- initializing all components from vernac downwards (no stm)

This commit moves stm specific arguments parsing to stm/stmargs.ml

[numeral] [plugins] Switch from `Big_int` to ZArith.

2020-08-27T17:03:33+00:00

We replace Coq's use of `Big_int` and `num` by the ZArith OCaml
library which is a more modern version.

We switch the core files and easy plugins only for now, more complex
numerical plugins will be done in their own commit.

We thus keep the num library linked for now until all plugins are
ported.

Co-authored-by: Vincent Laporte

Refining out the Refiner.

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

[declare] [api] Removal of deprecated functions

2020-06-26T12:38:10+00:00

The previous refactoring in `Declare` to add `CInfo.t` makes this a
good moment to clean overlays up w.r.t. deprecation.

All cases but one is just a matter of simple renaming, for the other
the use of an internal API is replaced by newer API.

Merge Clenvtac into Clenv.

2020-06-24T13:38:24+00:00

Having two different modules led to the availability of internal API in
the mli.

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

Rename files with Class in their name to make their role clearer.

2019-12-22T17:28:41+00:00

We restrict to those that are actually related to typeclasses, and
perform the following renamings:

Classops --> Coercionops
Class --> ComCoercion

[error] Remove special error printing pre-processing

2019-07-06T22:57:28+00:00

We remove the special error printing pre-processing in favor of just
calling the standard printers.

Error printing has been a bit complex for a while due to an incomplete
migration to a new printing scheme based on registering exception
printers; this PR should alleviate that by completing the registration
approach.

After this cleanup, it should not be ever necessary for normal
functions to worry a lot about catching errors and re-raising them,
unless they have some very special needs.

This change also allows to consolidate the `explainErr` and `himsg`
modules into one, removing the need to export the error printing
functions. Ideally we would make the contents of `himsg` more
localized, but this can be done in a gradual way.