X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Ftypes.ma;h=586ce31ce7bb527d251d3d1a9ddf5704f9163a2a;hb=44c1079dabf1d3c0b69d0155ddbaea8627ec901c;hp=0fd4eb5886cb0d067459a47b9c5703c5b48e413e;hpb=1410ea677188e9e11d748c69e208d1e90b0a324e;p=helm.git

diff --git a/weblib/basics/types.ma b/weblib/basics/types.ma
index 0fd4eb588..586ce31ce 100644
--- a/weblib/basics/types.ma
+++ b/weblib/basics/types.ma
@@ -58,4 +58,4 @@ inductive option (A:Type[0]) : Type[0] ≝
 inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝
   dp: ∀a:A.(f a)→Sig A f.
 
-interpretation "Sigma" 'sigma x = (Sig ? x).
+interpretation "Sigma" 'sigma x = (Sig ? x).
\ No newline at end of file