From 2debc4ab0b171963afff40cc3183e4e92cca9a0e Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 22 Jul 2008 14:02:22 +0000
Subject: Correct implementation of discharging of implicit arguments and add
 new setting "Set Manual Implicit Arguments" for manual-only implicits. Fix
 test-suite script. This removes the discharge_info argument of "dynamic"
 object's rebuild function.

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

(limited to 'test-suite')

diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index e7795733f6..84ec298df9 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -2,6 +2,8 @@ Inductive vector {A : Type} : nat -> Type :=
 | vnil : vector 0
 | vcons : A -> forall {n'}, vector n' -> vector (S n').
 
+Implicit Arguments vector [].
+
 Require Import Coq.Program.Program.
 
 Program Definition head {A : Type} {n : nat} (v : vector A (S n)) : vector A n :=
-- 
cgit v1.2.3