coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-09-29	Almost fully moving funind to new proof engine.	Hugo Herbelin

2020-04-10	[ocamlformat] Enable for funind.	Emilio Jesus Gallego Arias
	As part of the proof refactoring work I am doing some modifications to `funind` and indentation of that code is driving me a bit crazy; I'd much prefer to delegate it to an automatic tool.
2017-07-17	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias

2017-06-16	Removing Proof_type from the API.	Pierre-Marie Pédrot
	Unluckily, this forces replacing a lot of code in plugins, because the API defined the type of goals and tactics in Proof_type, and by the no-alias rule, this was the only one. But Proof_type was already implicitly deprecated, so that the API should have relied on Tacmach instead.
2017-06-10	Remove (useless) aliases from the API.	Matej Košík

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

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

2017-04-22	Merge branch v8.6 into trunk	Hugo Herbelin
	Note: I removed what seemed to be dead code in recdef.ml (local_assum and local_def introduced with econstr branch), assuming that this is what should be done.
2017-04-04	Solving first problem in bug #4306. TO DO : solve the let in problem	Julien Forest

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

2015-12-07	Fix some typos.	Guillaume Melquiond

2015-04-14	Function now supports puniveres	jforest

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