coq/plugins/ring, branch master

[build] Split stdlib to it's own opam package.

2021-03-03T15:06:14+00:00

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.

Improve some error messages.

2020-11-16T19:30:08+00:00

This also includes aligning with refman when relevant and using capital
letters and final period.

Other renamings evd -> sigma in newring.ml.

2020-11-16T17:24:02+00:00

Pass sigma functionally in newring.ml.

2020-11-16T17:24:02+00:00

{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`.

Legacy Ring and Legacy Field migrated to contribs

2012-07-05T22:51:11+00:00

 One slight point to check someday : fourier used to
 launch a tactic called Ring.polynom in some cases.
 It it crucial ? If so, how to replace with the setoid_ring
 equivalent ?

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7

Kills the useless tactic annotations "in |- *"

2012-07-05T16:56:37+00:00

 Most of these heavyweight annotations were introduced a long time ago
 by the automatic 7.x -> 8.0 translator

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7

Open Local Scope ---> Local Open Scope, same with Notation and alii

2012-07-05T16:56:28+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7

ZArith + other : favor the use of modern names instead of compat notations

2012-07-05T16:56:16+00:00

 - For instance, refl_equal --> eq_refl
 - Npos, Zpos, Zneg now admit more uniform qualified aliases
   N.pos, Z.pos, Z.neg.
 - A new module BinInt.Pos2Z with results about injections from
   positive to Z
 - A result about Z.pow pushed in the generic layer
 - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
 - Using tactic Z.le_elim instead of Zle_lt_or_eq
 - Some cleanup in ring, field, micromega
   (use of "Equivalence", "Proper" ...)
 - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
 - In ZMake and ZMake, functor parameters are now named NN and ZZ
   instead of N and Z for avoiding confusions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7

place all files specific to camlp4 syntax extensions in grammar/

2012-05-29T11:09:25+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15387 85f007b7-540e-0410-9357-904b9bb8a0f7