coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-03-03	[build] Split stdlib to it's own opam package.	Emilio Jesus Gallego Arias
	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.
2020-11-20	A step towards supporting pattern cast deeplier.	Hugo Herbelin
	We at least support a cast at the top of patterns in notations.
2020-11-20	Add preliminary support for notations with large class (non-recursive) binders.	Hugo Herbelin
	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".
2020-11-04	Remove warning on SSR Search having moved.	Théo Zimmermann

2020-07-03	Fix #11121: Simultaneous definition of term and notation in custom grammar	Maxime Dénès

2020-05-28	Adding missing DECLARE PLUGIN so that compilation with -natdynlink no works.	Hugo Herbelin

2020-05-18	[search] [ssr] Emit deprecated message when calling search from ssreflect	Emilio Jesus Gallego Arias
	but ssrsearch is not loaded. Fixes #12338
2020-05-15	Cleaning the use of pstate and evar_map in Search.	Hugo Herbelin

2020-05-15	Move SSR's Search to a new plugin and deprecate it.	Théo Zimmermann