coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-10-02	{new,setoid_}ring -> ring	Maxime Dénès
	I believe this renaming makes it easier for new contributors to discover the code of `ring`.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-05-24	Stop using pstate in global print queries	Gaëtan Gilbert
	Using pstate makes no sense for printing global stuff
2018-06-21	Further cleanup: do not export the closed_term Ltac entry.	Pierre-Marie Pédrot
	We only use it locally, so we simply register the ML tactic inside the module but we do not export the syntax.
2018-05-04	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias
	In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at.
2018-02-27	Update headers following #6543.	Théo Zimmermann

2017-07-17	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias

2017-06-07	Put all plugins behind an "API".	Matej Kosik

2017-04-27	Remove unused [open] statements	Gaetan Gilbert

2017-02-14	Setoid_ring API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Quote API using EConstr.	Pierre-Marie Pédrot

2016-06-24	Removing tactic compatibility layers in setoid_ring.	Pierre-Marie Pédrot

2016-05-04	Moving the Val module to Geninterp.	Pierre-Marie Pédrot

2016-02-22	The tactic generic argument now returns a value rather than a glob_expr.	Pierre-Marie Pédrot
	The glob_expr was actually always embedded as a VFun, so this patch should not change anything semantically. The only change occurs in the plugin API where one should use the Tacinterp.tactic_of_value function instead of Tacinterp.eval_tactic. Moreover, this patch allows to use tactics returning arguments from the ML side.
2015-01-25	Adding a proper interface to Newring.	Pierre-Marie Pédrot
	The ring ASTs were put in a separate interface, and only the extension-related code was put in a dedicated G_newring file.