diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-03 17:15:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-04 18:42:22 +0200 |
| commit | e1e0f4f7f3c549fd3d5677b67c6b13ed687e6f12 (patch) | |
| tree | 70d40db0a8bb6378bb97d9c7c72567045bd4bd78 /theories/Reals/NewtonInt.v | |
| parent | 6c9e2ded8fc093e42902d008a883b6650533d47f (diff) | |
Make standard library independent of the names generated by
induction/elim over a dependent elimination principle for Prop
arguments.
Diffstat (limited to 'theories/Reals/NewtonInt.v')
| -rw-r--r-- | theories/Reals/NewtonInt.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index 928422ed8..e0bb8ee2b 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -98,7 +98,7 @@ Lemma NewtonInt_P5 : Newton_integrable (fun x:R => l * f x + g x) a b. Proof. unfold Newton_integrable; intros f g l a b X X0; - elim X; intros; elim X0; intros; + elim X; intros x p; elim X0; intros x0 p0; exists (fun y:R => l * x y + x0 y). elim p; intro. elim p0; intro. |