X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fcpr0_defs.v;h=7773a3410ced2759291a097635e787ed113ad5d2;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=5434debd467a03b929b9e2033d65d99e5a84ea78;hpb=a8052b7482d5573eca2776ea11cb7a4b06236fbd;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/cpr0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/cpr0_defs.v
index 5434debd4..7773a3410 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/cpr0_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/cpr0_defs.v
@@ -3,7 +3,7 @@ Require Export drop_defs.
 Require Export pr0_defs.
 
 (*#* #caption "current axioms for the relation $\\CprZ{}{}$",
-   "reflexivity", "compaibility" 
+   "reflexivity", "compatibility" 
 *)
 (*#* #cap #cap c, c1, c2 #alpha u1 in V1, u2 in V2, k in z *)