diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-18 15:03:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-18 15:03:24 +0000 |
| commit | 2c69928079fcbafcdd8c2d540d95905bdbf0d58c (patch) | |
| tree | 9ab27da9dd9858fcec7e7b772c5213880625bcf0 /test-suite/success | |
| parent | 52210a54bd994ae3965c10391fa7bf29b74e6c56 (diff) | |
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
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/implicit.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index b28653831..e8019a908 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. |