From 8e069e6b19c5c2509f2fb4dd226672ce7342e533 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 23 Feb 2015 12:45:04 +0100
Subject: [PATCH] infprod RA: explain types
---
lib/ModuRes/RA.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/lib/ModuRes/RA.v b/lib/ModuRes/RA.v
index 1d690ad32..3774ff661 100644
--- a/lib/ModuRes/RA.v
+++ b/lib/ModuRes/RA.v
@@ -369,6 +369,7 @@ End Agreement.
Section InfiniteProduct.
+ (* S is the index type (domain), T the type of the components (codomain) *)
Context (S T : Type) `{RA_T : RA T}.
Local Open Scope ra_scope.
--
GitLab