coq - The formal proof system

Age	Commit message (Collapse)	Author
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-01-24	Make `Instance` without a body always open a proof.	Maxime Dénès

2018-02-27	Update headers following #6543.	Théo Zimmermann

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2016-11-03	typeclasses eauto Implem/doc of shelving strategy	Matthieu Sozeau
	Now [typeclasses eauto] mimicks what happens during resolution faithfully, and the shelving behavior/requirements for a successful proof-search are documented.
2016-11-03	Fix handling of only_classes at toplevel	Matthieu Sozeau

2016-10-05	Clean up type classes flags and update compat file.	Maxime Dénès

2016-06-16	Purely refactoring and code/API cleanup.	Matthieu Sozeau
	Fix test-suite files
2016-06-16	eauto: fix test-suite file	Matthieu Sozeau
	Now that typeclasses eauto uses the new eauto.
2016-06-16	Fix iterative deepening strategy failing too early	Matthieu Sozeau
	Report limit exceeded on _any_ branch so that we pursue search if it was reached at least once. Add example by N. Tabareau in test-suite.
2016-06-16	Implement limited proof search and iterative deepening.	Matthieu Sozeau
	Fix typo in proofview
2016-06-16	Typeclasses eauto based on new proof engine,	Matthieu Sozeau
	with full backtracking across multiple goals.
2016-01-20	Update copyright headers.	Maxime Dénès

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

2012-08-08	Updating headers.	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 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
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
2005-12-21	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16	Nouvelle en-tête	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11	Ajout d'un vieil exemple de N. Magaud	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5457 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15	entetes	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-27	Ajout d'un test sur EAuto	mohring
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1408 85f007b7-540e-0410-9357-904b9bb8a0f7