From 57eec1e1e4efd09f5181297d87b1908c284e6951 Mon Sep 17 00:00:00 2001 From: notin Date: Wed, 26 Mar 2008 17:22:36 +0000 Subject: Diverses petites modifs dans la test-suite: test-suite/output/ZSyntax.out typo test-suite/bugs/closed/shouldsucceed/1776.v bug closed test-suite/success/extraction.v test-suite/success/extraction.v test-suite/bugs/closed/shouldsucceed/846.v backtrack sur le commit 10639 test-suite/bugs/closed/shouldsucceed/1322.v: petites modifications suite aux changement de setoid_replace test-suite/bugs/closed/shouldsucceed/1414.v: petites modifications suite aux changement dans Program git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10723 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/success/extraction.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/success') diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 6a5bf58b64..74d87ffa7e 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -322,7 +322,7 @@ Extraction test24. Require Import Gt. Definition loop (Ax:Acc gt 0) := (fix F (a:nat) (b:Acc gt a) {struct b} : nat := - F (S a) (Acc_inv b (gt_Sn_n a))) 0 Ax. + F (S a) (Acc_inv b (S a) (gt_Sn_n a))) 0 Ax. Extraction loop. (* let loop _ = let rec f a = -- cgit v1.2.3