From fe4df66869250943913c7fa534bb22305a320683 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 9 Mar 2011 11:59:38 +0000
Subject: [PATCH] the interpretation for Sigma was missing

---
 matita/matita/lib/basics/types.ma | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index c14cc60b4..08b99a8cb 100644
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -56,4 +56,6 @@ inductive option (A:Type[0]) : Type[0] ≝
 
 (* sigma *)
 inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝
-  dp: ∀a:A.(f a)→Sig A f.
\ No newline at end of file
+  dp: ∀a:A.(f a)→Sig A f.
+  
+interpretation "Sigma" 'sigma x = (Sig ? x).
-- 
2.39.5