coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[stdlib] Do not use deprecated notations	Vincent Laporte	2018-03-06
\|
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Fixing bug #4186.	Pierre-Marie Pédrot	2015-04-13
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Extraction: qualified names in Extract Constant examples (fix #2878)	letouzey	2012-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16089 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed my last patch: these files no longer use nat_beq (automatically	vsiles	2011-05-16
\| \| \| \| \| \| \| \|	generated) but rather use beq_nat (Arith.EqNat) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14126 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extraction: finish ExtrOcamlNatInt, add similar translation nat==>big_int	letouzey	2010-06-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13074 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extraction: start of a support library	letouzey	2010-06-02
	- ExtrOcamlBasic: mapping of basic types to ocaml's ones - ExtrOcamlIntConv: conversion between int and coq's numerical types - ExtrOcamlBigIntConv: same with big_int (no overflow) - ExtrOcamlNatInt: realizes nat by int (unsafe) more to come: Haskell, handling of stings, more stuff in ExtrOcamlNatInt, etc etc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13050 85f007b7-540e-0410-9357-904b9bb8a0f7