From 2c69928079fcbafcdd8c2d540d95905bdbf0d58c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 18 Dec 2011 15:03:24 +0000
Subject: Fixed a Not_found bug when declaring in a section some implicit
 arguments for a constant not defined in the section.

Also fixed some typos in the doc of implicit arguments in the
reference manual.

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

(limited to 'test-suite')

diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index b286538316..e8019a908f 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -120,3 +120,7 @@ Check C2 eq_refl.
 
 Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop :=
  | C3 : I3 a (n:=0).
+
+(* Check global implicit declaration over ref not in section *)
+
+Section D. Global Arguments eq [A] _ _. End D.
-- 
cgit v1.2.3