Merge pull request #85 from coq-community/function_scope

Adapt to math-comp/math-comp#1131

refinements/examples/irred.v

@@ -196,15 +196,15 @@ Section enumerable.
 Context (T : finType) (T' : Type) (RT : T -> T' -> Type).
 Variable (N : Type) (rN : nat -> N -> Type).
 Context (enumT' : seq T')
-  {enumR : refines (perm_eq \o (list_R RT)) (@Finite.enum T) enumT'}.
+  {enumR : refines (perm_eq \o list_R RT) (@Finite.enum T) enumT'}.
 Context `{zero_of N} `{one_of N} `{add_of N}.
 Context `{!refines rN 0%N 0%C}.
 Context `{!refines rN 1%N 1%C}.
-Context `{!refines (rN ==> rN ==> rN)%rel addn add_op}.
+Context `{!refines (rN ==> rN ==> rN) addn add_op}.
 Context (P : pred T) (P' : pred T').
 
 #[export] Instance refines_card :
-  (forall x x' `{!refines RT x x'}, refines (bool_R \o (@unify _)) (P x) (P' x')) ->
+  (forall x x' `{!refines RT x x'}, refines (bool_R \o @unify _) (P x) (P' x')) ->
   refines rN #|[pred x | P x]| (card' enumT' P').
 Proof.
 move=> RP; have := refines_comp_unify (RP _ _ _) => /refines_abstr => {}RP.
@@ -274,13 +274,13 @@ Context (iter' : forall T, N -> (T -> T) -> T -> T)
   {iterR : forall T T' RT,
     refines (rN ==> (RT ==> RT) ==> RT ==> RT) (@iter T) (@iter' T')}.
 Context (enumC : seq C)
-  {enumR : refines (perm_eq \o (list_R rAC)) (@Finite.enum A) enumC}.
+  {enumR : refines (perm_eq \o list_R rAC) (@Finite.enum A) enumC}.
 
 Definition Rnpoly : {poly_n A} -> {poly A} -> Type :=
   fun p q => p = q :> {poly A}.
 
 Definition RnpolyC : {poly_n A} -> seqpoly C -> Type :=
-  (Rnpoly \o (RseqpolyC rAC))%rel.
+  (Rnpoly \o RseqpolyC rAC)%rel.
 
 #[export] Instance refines_enum_npoly :
    refines (perm_eq \o list_R RnpolyC)

refinements/refinements.v

@@ -205,6 +205,7 @@ Qed.
 
 End refinements.
 
+Arguments refines [A B]%type R%rel m n.
 Arguments refinesP {T T' R x y} _.
 
 #[export] Hint Mode refines - - - + - : typeclass_instances.

refinements/seqmx.v

@@ -666,7 +666,7 @@ Qed.
        (rn : nat_R n1 n2) f g
        `{forall x y, refines (rI rm) x y ->
          forall z t, refines (rI rn) z t ->
-         refines (rAC \o (@unify _)) (f x z) (g y t)} :
+         refines (rAC \o @unify _) (f x z) (g y t)} :
   refines (RseqmxC rm rn)
           (\matrix_(i, j) f i j) (seqmx_of_fun (I:=I) g).
 Proof.
@@ -680,7 +680,7 @@ Qed.
 #[export] Instance refine_seqmx_of_fun m n f g
        `{forall x y, refines (rI (nat_Rxx m)) x y ->
          forall z t, refines (rI (nat_Rxx n)) z t ->
-         refines (rAC \o (@unify _)) (f x z) (g y t)} :
+         refines (rAC \o @unify _) (f x z) (g y t)} :
   refines (RseqmxC (nat_Rxx m) (nat_Rxx n))
           (\matrix_(i, j) f i j) (seqmx_of_fun (I:=I) g).
 Proof. exact: RseqmxC_seqmx_of_fun. Qed.

refinements/seqpoly.v

@@ -460,7 +460,7 @@ Context `{!refines (rN ==> rN ==> bool_R) eqtype.eq_op eq_op}.
 Context `{!refines (rN ==> nat_R) spec_id spec}.
 
 Definition RseqpolyC : {poly R} -> seq C -> Type :=
-  (Rseqpoly \o (list_R rAC)).
+  (Rseqpoly \o list_R rAC)%rel.
 
 #[export] Instance RseqpolyC_cons :
   refines (rAC ==> RseqpolyC ==> RseqpolyC) (@cons_poly R) cons.