← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to test-suite/ideal-features/universes.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
test-suite/ideal-features/universes.v
 
1
(* Some issues with polymorphic inductive types *)
 
2
 
 
3
(* 1- upper constraints with respect to non polymorphic inductive types *)
 
4
 
 
5
Unset Elimination Schemes.
 
6
Definition Ty := Type (* Top.1 *).
 
7
 
 
8
Inductive Q (A:Type (* Top.2 *)) : Prop := q : A -> Q A.
 
9
Inductive T (B:Type (* Top.3 *)) := t : B -> Q (T B) -> T B.
 
10
(* ajoute Top.4 <= Top.2 inutilement: 
 
11
   4 est l'univers utilisé dans le calcul du type polymorphe de T *)
 
12
Definition C := T Ty.
 
13
(* ajoute Top.1 < Top.3 :
 
14
   Top.3 jour le rôle de pivot pour propager les contraintes supérieures qu'on
 
15
   a sur l'argument B de T: Top.3 sera réutilisé plus tard comme majorant
 
16
   des arguments effectifs de T, propageant à cette occasion les contraintes
 
17
   supérieures sur Top.3 *)
 
18
 
 
19
(* We need either that Q is polymorphic on A (though it is in Type) or
 
20
   that the constraint Top.1 < Top.2 is set (and it is not set!) *)
 
21
 
 
22
(* 2- upper constraints with respect to unfoldable constants *)
 
23
 
 
24
Definition f (A:Type (* Top.1 *)) := True.
 
25
Inductive R := r : f R -> R.
 
26
(* ajoute Top.3 <= Top.1 inutilement: 
 
27
   Top.3 est l'univers utilisé dans le calcul du type polymorphe de R *)
 
28
 
 
29
(* mais il manque la contrainte que l'univers de R est plus petit que Top.1
 
30
   ce qui l'empêcherait en fait d'être vraiment polymorphe *)
 
31
 
 
32
(* 3- constraints with respect to global constants *)
 
33
 
 
34
Inductive S (A:Ty) := s : A -> S A.
 
35
 
 
36
(* Q est considéré polymorphique vis à vis de A alors que le type de A
 
37
   n'est pas une variable mais un univers déjà existant *)
 
38
 
 
39
(* Malgré tout la contrainte Ty < Ty est ajoutée (car Ty est vu comme
 
40
   un pivot pour propager les contraintes sur le type A, comme si Q était
 
41
   vraiment polymorphique, ce qu'il n'est pas parce que Ty est une
 
42
   constante). Et heureusement qu'elle est ajouté car elle évite de
 
43
   pouvoir typer "Q Ty" *)