coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
\| \| \| \|	We do up to `Term` which is the main bulk of the changes.
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
\|
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
\|
*	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin	2017-03-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information.
*	Function now supports puniveres	jforest	2015-04-14
\|
*	handling Functional Scheme for required but not imported modules	Julien Forest	2014-12-11
\|
*	Modulification of name	ppedrot	2012-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modulification of identifier	ppedrot	2012-12-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rename files in funind to respect new conventions	glondu	2010-12-24
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13755 85f007b7-540e-0410-9357-904b9bb8a0f7