diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-06-02 15:06:46 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-06-02 15:06:46 +0000 |
commit | fc1029dc524df57d95b5fe886bb69dc5058fe517 (patch) | |
tree | 9512920c7c30b9622c6a8ed04ac1d9bf0765b0e9 | |
parent | 057689a3897b85e5f68e1f112467ad40600cc965 (diff) |
Ajout tests
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5787 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | test-suite/success/coercions.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index 98b613ba3..17c4f9078 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -9,3 +9,24 @@ Coercion f: S >-> Z. Parameter g : Z -> Z. Check [s](g (s::S)). + + +(* Check uniform inheritance condition *) + +Parameter h : nat -> nat -> Prop. +Parameter i : (n,m:nat)(h n m) -> nat. +Coercion i : h >-> nat. + +(* Check coercion to funclass when the source occurs in the target *) + +Parameter C: nat -> nat -> nat. +Coercion C : nat >-> FUNCLASS. + +(* Remark: in the following example, it cannot be decide whether C is + from nat to Funclass or from A to nat. An explicit Coercion command is + expected + +Parameter A : nat -> Prop. +Parameter C:> forall n:nat, A n -> nat. +*) + |