compiles with Coq 8.8 and SSR dev from 23/05/2018

math-comp · Jul 17, 2018 · 59c4349 · 59c4349
1 parent d441188
commit 59c4349
Show file tree

Hide file tree

Showing 7 changed files with 12 additions and 12 deletions.
diff --git a/auxresults/auxresults.v b/auxresults/auxresults.v
@@ -508,7 +508,7 @@ End MorePath.
 
 Section MoreFinmap.
 
-Open Local Scope fset_scope.
+Local Open Scope fset_scope.
 
 Lemma finSet_notin_ind (T : choiceType) (P : {fset T} -> Prop) : 
   P fset0 -> (forall s x, P s -> x \notin s -> P (x |` s)) -> forall s, P s.

diff --git a/coq-ssr-elliptic-curves/polyall.v b/coq-ssr-elliptic-curves/polyall.v
@@ -13,7 +13,7 @@ From mathcomp Require Export polyorder.
 
 Import GRing.Theory.
 
-Open Local Scope ring_scope.
+Local Open Scope ring_scope.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

diff --git a/coq-ssr-elliptic-curves/polydec.v b/coq-ssr-elliptic-curves/polydec.v
@@ -12,7 +12,7 @@ From mathcomp Require Import ssrfun choice tuple fintype bigop.
 
 Import GRing.Theory.
 
-Open Local Scope ring_scope.
+Local Open Scope ring_scope.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

diff --git a/newtonsums/expansiblefracpoly.v b/newtonsums/expansiblefracpoly.v
@@ -25,7 +25,7 @@ Unset Printing Implicit Defensive.
 
 Import GRing.Theory.
 Local Open Scope ring_scope.
-Open Local Scope quotient_scope.
+Local Open Scope quotient_scope.
 
 Section ExpansibleFracpoly.
 

diff --git a/newtonsums/fracrev.v b/newtonsums/fracrev.v
@@ -14,8 +14,8 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Import GRing.Theory.
-Open Local Scope ring_scope.
-Open Local Scope quotient_scope.
+Local Open Scope ring_scope.
+Local Open Scope quotient_scope.
 
 Reserved Notation "{ 'fracpoly' T }" (at level 0, format "{ 'fracpoly'  T }").
 Reserved Notation "x %:F" (at level 2, format "x %:F").

diff --git a/newtonsums/fraction.v b/newtonsums/fraction.v
@@ -16,8 +16,8 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Import GRing.Theory.
-Open Local Scope ring_scope.
-Open Local Scope quotient_scope.
+Local Open Scope ring_scope.
+Local Open Scope quotient_scope.
 
 Reserved Notation "{ 'ratio' T }" (at level 0, format "{ 'ratio'  T }").
 Reserved Notation "{ 'fraction' T }" (at level 0, format "{ 'fraction'  T }").

diff --git a/semialgebraic/semialgebraic.v b/semialgebraic/semialgebraic.v
@@ -1108,7 +1108,7 @@ Proof.
 move : s; apply : quotP => f hf.
 rewrite /SA_all_proj; unlock.
 apply/eqP; rewrite eqmodE hf.
-apply/rcf_satP/nforallP => u; rewrite cat0s.
+apply/rcf_satP/nforallP => u; rewrite cat0s /=.
 split=> h x.
 + by move/(_ x)/holds_repr_pi/(_ x) : h; rewrite set_set_nth eqxx.
 + apply/holds_repr_pi => y; rewrite set_set_nth eqxx.
@@ -3437,9 +3437,9 @@ Fail Fixpoint test (p : {poly F}) :=
                      else (test p^`())*(2%:R).
 
 Check (fun (p : {poly F}) => if (size p <= 1)%N then [::] else (polyrcf.rootsR p)).
-Fixpoint vroot (p : {poly F}) := 
-  if (size p <= 1)%N then [::] 
-                     else let s := vroot (p^`()) in (polyrcf.rootsR p).
+(* Fixpoint vroot (p : {poly F}) :=  *)
+(*   if (size p <= 1)%N then [::]  *)
+(*                      else let s := vroot (p^`()) in (polyrcf.rootsR p). *)
 
 (* Variables (A : choiceType) (x : {fset A}) (P : pred A) (a : A) (ha : P a) (i : nat). *)
 (* Check (unpickle P i x). *)