Skip to content

GitLab

Commit ca346a48 authored by Ralf Jung's avatar Ralf Jung
Browse files
Options

remove unnecessary backticks

parent aecd5422
Hide whitespace changes
Inline Side-by-side
Showing with 5 additions and 5 deletions
lib/ModuRes/RA.v
View file @ ca346a48
......@@ -376,11 +376,11 @@ End Agreement.
Section InfiniteProduct.
(* I is the index type (domain), S the type of the components (codomain) *)
Context (I : Type) (S : forall (i : I), Type)
`{tyS : forall i, Setoid (S i)}
`{uS : forall i, RA_unit (S i)}
`{opS : forall i, RA_op (S i)}
`{vS : forall i, RA_valid (S i)}
`{raS : forall i, RA (S i)}.
{tyS : forall i, Setoid (S i)}
{uS : forall i, RA_unit (S i)}
{opS : forall i, RA_op (S i)}
{vS : forall i, RA_valid (S i)}
{raS : forall i, RA (S i)}.
Local Open Scope ra_scope.
Definition ra_res_infprod := forall (i : I), S i.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment