From a28e2d94c7a0ee0c85d7f018115ffc2c64e62d5f Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 12 Mar 2010 16:40:02 +0000
Subject: fixed minor pbs with test cases

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12865 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/complexity/guard.v  | 2 +-
 test-suite/success/Inductive.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/test-suite/complexity/guard.v b/test-suite/complexity/guard.v
index f64ffc2598..387263e2f3 100644
--- a/test-suite/complexity/guard.v
+++ b/test-suite/complexity/guard.v
@@ -1,6 +1,6 @@
 (* Examples to check that the guard condition does not unfold
    irrelevant subterms *)
-(* Expected time < 1s *)
+(* Expected time < 1.00s *)
 Require Import Bool.
 
 Fixpoint slow n :=
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 8ffe4fcdb2..41819d9219 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -56,11 +56,11 @@ Check
 
 (* Check inductive types with local definitions (constructors) *)
 
-Inductive I1 : Set := c (_:I1) (_:=0).
+Inductive I1 : Set := C1 (_:I1) (_:=0).
 
 Check (fun x:I1 =>
   match x with
-  | c i n => (i,n)
+  | C1 i n => (i,n)
   end).
 
 (* Check implicit parameters of inductive types (submitted by Pierre
-- 
cgit v1.2.3