X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr0_defs.v;h=640b56f1f02fd01759f4870f8d2a69b4b93b9ede;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=a2180b9d1401b48b5ea0405046200465b13c5873;hpb=50cfabb6b8136873a02f8fd1512f0b62f97e2639;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v
index a2180b9d1..640b56f1f 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v
@@ -1,7 +1,7 @@
 Require Export subst0_defs.
 
 (*#* #caption "axioms for the relation $\\PrZ{}{}$",
-   "reflexivity", "compaibility", "$\\beta$-contraction", "$\\upsilon$-swap", 
+   "reflexivity", "compatibility", "$\\beta$-contraction", "$\\upsilon$-swap", 
    "$\\delta$-expansion", "$\\zeta$-contraction", "$\\epsilon$-contraction"
 *)
 (*#* #cap #cap t, t1, t2 #alpha u in V, u1 in V1, u2 in V2, v1 in W1, v2 in W2, w in T, k in z *)