diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-26 15:58:32 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-26 15:58:32 +0000 |
| commit | d081dcfaedb5b7e2ad78574a053bcebc4bfb564a (patch) | |
| tree | dfdb78d703b6eb48d43b4ca555a3fd24e37db574 /theories/Program/Wf.v | |
| parent | e467f77a19229058070d43e9cf1080534b9aee74 (diff) | |
Proper implicit arguments handling for assumptions
(Axiom/Variable...). New tactic clapply to apply unapplied class methods
in tactic mode, simple solution to the fact that apply does not work
up-to classes yet. Add Functions.v for class definitions related to
functional morphisms.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10589 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 70b1b1b5a..98b18f903 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -17,7 +17,7 @@ Section Well_founded. Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x := F_sub x (fun y: { y : A | R y x} => Fix_F_sub (proj1_sig y) - (Acc_inv r (proj1_sig y) (proj2_sig y))). + (Acc_inv r (proj2_sig y))). Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x). End Acc. @@ -38,7 +38,7 @@ Section Well_founded. Lemma Fix_F_eq : forall (x:A) (r:Acc R x), - F_sub x (fun (y:A|R y x) => Fix_F (`y) (Acc_inv r (proj1_sig y) (proj2_sig y))) = Fix_F x r. + F_sub x (fun (y:A|R y x) => Fix_F (`y) (Acc_inv r (proj2_sig y))) = Fix_F x r. Proof. destruct r using Acc_inv_dep; auto. Qed. @@ -89,7 +89,7 @@ Section Well_founded_measure. Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x := F_sub x (fun y: { y : A | m y < m x} => Fix_measure_F_sub (proj1_sig y) - (Acc_inv r (m (proj1_sig y)) (proj2_sig y))). + (@Acc_inv _ _ _ r (m (proj1_sig y)) (proj2_sig y))). Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)). @@ -111,7 +111,7 @@ Section Well_founded_measure. Lemma Fix_measure_F_eq : forall (x:A) (r:Acc lt (m x)), - F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (m (proj1_sig y)) (proj2_sig y))) = Fix_F x r. + F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (proj2_sig y))) = Fix_F x r. Proof. intros x. set (y := m x). |