coq/plugins/ssrsearch, branch master The formal proof system [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.
A step towards supporting pattern cast deeplier. 2020-11-20T18:41:20+00:00 Hugo Herbelin 2020-10-24T11:18:09+00:00 23924afa0e4d7ed9ca58fbf5f69dc57685d593fa We at least support a cast at the top of patterns in notations. 
We at least support a cast at the top of patterns in notations.
Add preliminary support for notations with large class (non-recursive) binders. 2020-11-20T18:41:17+00:00 Hugo Herbelin 2020-10-23T20:58:30+00:00 52b93b587b9cb53b0ed11c7d6cf5f328d7ee1479 We introduce a class of open binders which includes "x", "x:t", "'pat" and a class of closed binders which includes "x", "(x:t)", "'pat". 
We introduce a class of open binders which includes "x", "x:t", "'pat"
and a class of closed binders which includes "x", "(x:t)", "'pat".
Remove warning on SSR Search having moved. 2020-11-04T11:38:31+00:00 Théo Zimmermann 2020-10-21T09:05:52+00:00 e047599a7851d5c757635e966067ca9271577692 






Fix #11121: Simultaneous definition of term and notation in custom grammar
2020-07-03T11:13:02+00:00

Maxime Dénès

2020-06-16T15:09:40+00:00

53e19f76624b7a18792af799e970e9478f8e90a9












Adding missing DECLARE PLUGIN so that compilation with -natdynlink no works.
2020-05-28T15:02:55+00:00

Hugo Herbelin

2020-05-28T14:47:30+00:00

19c8ac834c4f43b1fd0c49aad286a4e5bebf0ce5












[search] [ssr] Emit deprecated message when calling search from ssreflect
2020-05-18T10:19:58+00:00

Emilio Jesus Gallego Arias

2020-05-17T11:45:06+00:00

57c023fe6b5c7f97403d849f7ca618c98d1af1a4

but ssrsearch is not loaded.

Fixes #12338





but ssrsearch is not loaded.

Fixes #12338







Cleaning the use of pstate and evar_map in Search.
2020-05-15T16:22:00+00:00

Hugo Herbelin

2020-05-11T15:41:58+00:00

50374354b7ced786d68d45884295a4c770642123












Move SSR's Search to a new plugin and deprecate it.
2020-05-15T16:05:11+00:00

Théo Zimmermann

2020-05-11T15:41:58+00:00

023d189aa201c8d5c71bc7de3e98725273d01b4f