coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-05-10	No more local reduction functions in Reductionops.	Pierre-Marie Pédrot
	This is extracted from #9710, where we need the environment anyway to compute iota rules on inductive types with let-bindings. The commit is self-contained, so I think it could go directly in to save me a few rebases. Furthermore, this is also related to #11707. Assuming we split cbn from the other reduction machine, this allows to merge the "local" machine with the general one, since after this PR they will have the same type. One less reduction machine should make people happy.
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

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-07-04	Bump year in headers.	Pierre-Marie Pédrot

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

2017-04-24	Porting the firstorder plugin to the new tactic API.	Pierre-Marie Pédrot

2016-01-20	Update copyright headers.	Maxime Dénès

2015-01-12	Update headers.	Maxime Dénès

2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
	With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
2012-08-08	Updating headers.	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in ↵	letouzey
	grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
	- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵	letouzey
	user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7