aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/Funind.v
AgeCommit message (Collapse)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04functional inversion now takes a quatified hypothesis as first argumentjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9009 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04- completely new version of "functional inversion" using inversion onjforest
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
2006-06-23modifs de test-suite suite au passage des graphes de Function dans Typejforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8986 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-06+ ameliorating the tactic "functional induction"jforest
+ 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
2005-12-21Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-09New version of Functional Scheme and functional induction. Deals withcoq
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
2003-06-21Added a test for Functional Induction.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4195 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-28fixing a typo in the new Funinv.v test in test-suite/successcourtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3722 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27Adding tests for the "functional induction" facility.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3711 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 16:55:54 +0000