Update to mathcomp 1.9

drouhling · Jul 5, 2019 · c7a515e · c7a515e
1 parent 85d74c0
commit c7a515e
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/README.md b/README.md
@@ -5,7 +5,7 @@ principle.
 
 This branch requires the [mathcomp-analysis
 library](https://github.com/math-comp/analysis) and its dependencies and the
-[ssring.v](https://github.com/jasmin-lang/jasmin/blob/f1f8b193591d369296d5661f0ae8a09f3b6eaa9b/proofs/3rdparty/ssrring.v)
+[ssring.v](https://raw.githubusercontent.com/jasmin-lang/jasmin/f1f8b193591d369296d5661f0ae8a09f3b6eaa9b/proofs/3rdparty/ssrring.v)
 file from [jasmin](https://github.com/jasmin-lang/jasmin).
 
 It is organised as follows:

diff --git a/pendulum.v b/pendulum.v
@@ -132,7 +132,7 @@ by rewrite (splitr e%:num) ltr_add //; [apply/p2e1_sp2he|apply/p3e2_sp3he];
   apply: ball_ler (pme12_q _ _); rewrite ler_minl lerr // orbC.
 Qed.
 
-Lemma preimV_lek0_closed : closed (V @^-1` (<= k0)).
+Lemma preimV_lek0_closed : closed (V @^-1` (<= k0 : _ -> _)).
 Proof.
 by apply: closed_comp; [move=> ??; apply: V_continuous|apply: closed_le].
 Qed.