coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-12-27	[API] remove large file containing duplicate interfaces	Enrico Tassi
	... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
2017-12-26	[ide] [doc] Document tweak to Query call.	Emilio Jesus Gallego Arias

2017-12-15	[econstr] Switch constrintern API to non-imperative style.	Emilio Jesus Gallego Arias
	We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step desirable to progress with EConstr there.
2017-11-29	[lib] [api] Introduce record for `object_prefix`	Emilio Jesus Gallego Arias
	This is a minor cleanup adding a record in a try to structure the state living in `Lib`.
2017-11-07	[api] Remove 8.7 ML-deprecated functions.	Emilio Jesus Gallego Arias

2017-11-03	Merge PR #6047: A generic printer for ltac values	Maxime Dénès

2017-11-03	Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in ↵	Maxime Dénès
	dev/doc/changes.
2017-11-02	Using a specific function to register vernac printers.	Hugo Herbelin

2017-10-27	Mention the migration from Bugzilla to GitHub issues in dev/doc/changes.	Théo Zimmermann

2017-10-26	Passing around the flag for injection so that tactics calling inj at	Hugo Herbelin
	ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug #5281.
2017-10-10	[configure] Support for flambda flags.	Emilio Jesus Gallego Arias
	We add a new option to configure `-flambda-opts` to allow passing custom flags to flambda. Example: ``` ./configure -flambda-opts "-O3 -unbox-closures" ```
2017-10-06	Extract changes to the XML protocol from its doc	Théo Zimmermann

2017-08-29	Move dev/doc/changes to Markdown.	Théo Zimmermann
	And remove old French part. And move part about the plugin API to the right section.