X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Ftypes.ma;h=a07cf29ea0e9c23f862e5ce04b311a2db7a99b3b;hb=a5c551d0b7399f00e8eef3dfb06e2a0895eac3d4;hp=0fd4eb5886cb0d067459a47b9c5703c5b48e413e;hpb=b5f54d2815f446a999736abd0ffe80641596a5f6;p=helm.git

diff --git a/weblib/basics/types.ma b/weblib/basics/types.ma
index 0fd4eb588..a07cf29ea 100644
--- a/weblib/basics/types.ma
+++ b/weblib/basics/types.ma
@@ -39,7 +39,7 @@ interpretation "pair pi1" 'pi1b x y = (fst ? ? x y).
 interpretation "pair pi2" 'pi2b x y = (snd ? ? x y).
 
 theorem eq_pair_fst_snd: ∀A,B.∀p:A a title="Product" href="cic:/fakeuri.def(1)"×/a B.
-  p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p, a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p 〉.
+  p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p, a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p 〉.
 #A #B #p (cases p) // qed.
 
 (* sum *)
@@ -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