coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey	2017-06-14
*	Fix Funind test-suite file after patch by Pierre.	Matthieu Sozeau	2014-07-11
*	Comment in Funind.v test-suite file	Matthieu Sozeau	2014-05-06
*	- Fixes for canonical structure resolution (check that the initial term indee...	Matthieu Sozeau	2014-05-06
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	functional inversion now takes a quatified hypothesis as first argument	jforest	2006-07-04
*	- completely new version of "functional inversion" using inversion on	jforest	2006-07-04
*	modifs de test-suite suite au passage des graphes de Function dans Type	jforest	2006-06-23
*	+ ameliorating the tactic "functional induction"	jforest	2006-06-06
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-21
*	New version of Functional Scheme and functional induction. Deals with	coq	2004-02-09
*	Added a test for Functional Induction.	courtieu	2003-06-21
*	fixing a typo in the new Funinv.v test in test-suite/success	courtieu	2003-02-28
*	Adding tests for the "functional induction" facility.	bertot	2003-02-27