diff options
Diffstat (limited to 'theories/Program')
-rw-r--r-- | theories/Program/Basics.v | 4 | ||||
-rw-r--r-- | theories/Program/Equality.v | 2 | ||||
-rw-r--r-- | theories/Program/Wf.v | 6 |
3 files changed, 7 insertions, 5 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 22436de69..ab1eccee2 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -15,6 +15,8 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) +Set Universe Polymorphism. + (** The polymorphic identity function is defined in [Datatypes]. *) Arguments id {A} x. @@ -45,7 +47,7 @@ Definition const {A B} (a : A) := fun _ : B => a. (** The [flip] combinator reverses the first two arguments of a function. *) -Definition flip {A B C} (f : A -> B -> C) x y := f y x. +Monomorphic Definition flip {A B C} (f : A -> B -> C) x y := f y x. (** Application as a combinator. *) diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 323e80cc3..96345e154 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -263,7 +263,7 @@ Class DependentEliminationPackage (A : Type) := Ltac elim_tac tac p := let ty := type of p in - let eliminator := eval simpl in (elim (A:=ty)) in + let eliminator := eval simpl in (@elim (_ : DependentEliminationPackage ty)) in tac p eliminator. (** Specialization to do case analysis or induction. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index f6d795b94..d82fa602a 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -153,7 +153,7 @@ Section Fix_rects. Hypothesis equiv_lowers: forall x0 (g h: forall x: {y: A | R y x0}, P (proj1_sig x)), - (forall x p p', g (exist (fun y: A => R y x0) x p) = h (exist _ x p')) -> + (forall x p p', g (exist (fun y: A => R y x0) x p) = h (exist (*FIXME shouldn't be needed *) (fun y => R y x0) x p')) -> f g = f h. (* From equiv_lowers, it follows that @@ -231,10 +231,10 @@ Module WfExtensionality. Program Lemma fix_sub_eq_ext : forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R) (P : A -> Type) - (F_sub : forall x : A, (forall y:{y : A | R y x}, P y) -> P x), + (F_sub : forall x : A, (forall y:{y : A | R y x}, P (` y)) -> P x), forall x : A, Fix_sub A R Rwf P F_sub x = - F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub y). + F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (` y)). Proof. intros ; apply Fix_eq ; auto. intros. |