diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-06-02 18:13:02 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-06-02 18:13:02 +0000 |
| commit | a52b0929a8ed4ca3df088adfbc596815550b76ba (patch) | |
| tree | 4342f1b6176353a142f8212db015b8ec4466627a /theories/Program/Wf.v | |
| parent | e60c362019cfd786121d070fbfa9c77dd029b420 (diff) | |
Use Type instead of Set.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12160 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Program/Wf.v')
| -rw-r--r-- | theories/Program/Wf.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 497e60205..75bbc8fd8 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -121,7 +121,7 @@ Hint Resolve measure_wf. Section Fix_rects. - Variable A: Set. + Variable A: Type. Variable P: A -> Type. Variable R : A -> A -> Prop. Variable Rwf : well_founded R. @@ -220,7 +220,7 @@ Section Fix_rects. End Fix_rects. -(** Tactic to fold a definitions based on [Fix_measure_sub]. *) +(** Tactic to fold a definition based on [Fix_measure_sub]. *) Ltac fold_sub f := match goal with @@ -245,8 +245,8 @@ Module WfExtensionality. (** For a function defined with Program using a well-founded order. *) Program Lemma fix_sub_eq_ext : - forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R) - (P : A -> Set) + forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R) + (P : A -> Type) (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x), forall x : A, Fix_sub A R Rwf P F_sub x = |