coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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 ↵	Matthieu Sozeau	2014-05-06
\| \| \| \| \| \| \| \|	indeed unifies with the projected term, keeping track of universes). - Fix the [unify] tactic to fail properly. - Fix unification to disallow lowering a global Type(i) universe to Prop or Set.
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
\| \| \| \| \| \| \|	Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
*	functional inversion now takes a quatified hypothesis as first argument	jforest	2006-07-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9009 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- completely new version of "functional inversion" using inversion on	jforest	2006-07-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	inductive - bug correction in "Functional scheme" and "functional inversion": the function are now parsed as references and not indent - adding a zeta normalization function in rawtermops to zeta normalize graph constructions (not used for now) - Bug correction in generation of functional principle types (if an arguments of the function has a type which is a sort) - adding a new persistent table for functional induction informations (graph,...) - new save mechanism for functional induction principles (reuse of proofs when possible) - Minor bug correction in proof of principle. - Distinguishing building_principles (that is save them) and making then (just construct their proof term) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9000 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modifs de test-suite suite au passage des graphes de Function dans Type	jforest	2006-06-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8986 85f007b7-540e-0410-9357-904b9bb8a0f7
*	+ ameliorating the tactic "functional induction"	jforest	2006-06-06
\| \| \| \| \| \| \| \|	+ bug correction in proof of structural principles + up do to date test-suite/success/Funind.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8899 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New version of Functional Scheme and functional induction. Deals with	coq	2004-02-09
\| \| \| \| \| \| \| \|	more functions (higher order and polymorphic functions), the principle is a bit better. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5310 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a test for Functional Induction.	courtieu	2003-06-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4195 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixing a typo in the new Funinv.v test in test-suite/success	courtieu	2003-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3722 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adding tests for the "functional induction" facility.	bertot	2003-02-27
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3711 85f007b7-540e-0410-9357-904b9bb8a0f7