From 2835ca605db43fa26f26b63d1b267b60ab64e264 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 21 Mar 2005 08:22:02 +0000
Subject: Ajout Unset Implicit Arguments manquant

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6872 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/Inversion.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'test-suite/success')

diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index 40d45afde..2649617bc 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -86,6 +86,7 @@ Admitted.
 
 (* Used to failed at some time *)
 
+Unset Implicit Arguments.
 Parameter bar : (p,q:nat) p=q -> Prop.
 Inductive foo : nat -> nat -> Prop := 
   C : (a,b:nat)(Heq:a = b) (bar a b Heq) -> (foo a b).
-- 
cgit v1.2.3