From ca346a4809b5af30a7dff7c7d982533e9589d57a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 23 Feb 2015 14:09:19 +0100
Subject: [PATCH] remove unnecessary backticks
---
lib/ModuRes/RA.v | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/lib/ModuRes/RA.v b/lib/ModuRes/RA.v
index 6887102b9..74b939e96 100644
--- a/lib/ModuRes/RA.v
+++ b/lib/ModuRes/RA.v
@@ -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.
--
GitLab