diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-15 18:45:27 +0530 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-15 18:59:00 +0530 |
| commit | 8309a98096facfba448c9d8d298ba3903145831a (patch) | |
| tree | 38a09851cb687921193b4368a93eed34ccd55a58 /theories | |
| parent | 58153a5bc59bbde6534425d66a2fe5d9943eb44b (diff) | |
Correct restriction of vm_compute when handling universe polymorphic
definitions. Instead of failing with an anomaly when trying to do
conversion or computation with the vm's, consider polymorphic constants
as being opaque and keep instances around. This way the code is still
correct but (obviously) incomplete for polymorphic definitions and we
avoid introducing an anomaly. The patch does nothing clever, it only
keeps around instances with constants/inductives and compile constant
bodies only for non-polymorphic definitions.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init/Datatypes.v | 4 | ||||
| -rw-r--r-- | theories/Init/Specif.v | 8 | ||||
| -rw-r--r-- | theories/Program/Basics.v | 4 |
3 files changed, 7 insertions, 9 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index a04535f40..de615301d 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -342,8 +342,8 @@ Arguments identity_rect [A] a P f y i. (** Identity type *) -Polymorphic Definition ID := forall A:Type, A -> A. -Polymorphic Definition id : ID := fun A x => x. +Definition ID := forall A:Type, A -> A. +Definition id : ID := fun A x => x. Definition IDProp := forall A:Prop, A -> A. Definition idProp : IDProp := fun A x => x. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 47e302e32..1384901b7 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -21,19 +21,19 @@ Require Import Logic. Similarly [(sig2 A P Q)], or [{x:A | P x & Q x}], denotes the subset of elements of the type [A] which satisfy both [P] and [Q]. *) -(* Polymorphic *) Inductive sig (A:Type) (P:A -> Prop) : Type := +Inductive sig (A:Type) (P:A -> Prop) : Type := exist : forall x:A, P x -> sig P. -(* Polymorphic *) Inductive sig2 (A:Type) (P Q:A -> Prop) : Type := +Inductive sig2 (A:Type) (P Q:A -> Prop) : Type := exist2 : forall x:A, P x -> Q x -> sig2 P Q. (** [(sigT A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type. Similarly for [(sigT2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *) -(* Polymorphic *) Inductive sigT (A:Type) (P:A -> Type) : Type := +Inductive sigT (A:Type) (P:A -> Type) : Type := existT : forall x:A, P x -> sigT P. -(* Polymorphic *) Inductive sigT2 (A:Type) (P Q:A -> Type) : Type := +Inductive sigT2 (A:Type) (P Q:A -> Type) : Type := existT2 : forall x:A, P x -> Q x -> sigT2 P Q. (* Notations *) diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 4bc29a071..e5be0ca92 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -15,8 +15,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* Set Universe Polymorphism. *) - (** The polymorphic identity function is defined in [Datatypes]. *) Arguments id {A} x. @@ -47,7 +45,7 @@ Definition const {A B} (a : A) := fun _ : B => a. (** The [flip] combinator reverses the first two arguments of a function. *) -Monomorphic Definition flip {A B C} (f : A -> B -> C) x y := f y x. +Definition flip {A B C} (f : A -> B -> C) x y := f y x. (** Application as a combinator. *) |