From 7944955b892f0ffa70ecf92f83b372cddc5b867b Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 30 Mar 2008 22:30:44 +0000 Subject: Modifications diverses et variées : - Nouvel essai de prise en compte unfold dans apply (unification.ml) - Correction bug commit précédent (constrintern.ml) - Correction bug d'explication des evars non résolues (evarutil.ml) - Fenêtre de query coqide plus large (command_windows.ml) - Orthographe tauto (tauto.ml4) - Crédits (ConstructiveEpsilon.v) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10731 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Logic/ConstructiveEpsilon.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'theories') diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v index 322f2d9be..fe571779c 100644 --- a/theories/Logic/ConstructiveEpsilon.v +++ b/theories/Logic/ConstructiveEpsilon.v @@ -31,6 +31,8 @@ To use [Fix_F], we define a relation R and prove that if [exists n, P n] then 0 is accessible with respect to R. Then, by induction on the definition of [Acc R 0], we show [{n : nat | P n}]. *) +(** Based on ideas from Benjamin Werner and Jean-François Monin *) + (** Contributed by Yevgeniy Makarov *) Require Import Arith. -- cgit v1.2.3