ocaml 3.09 transition

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / pr0_defs.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v
index a2180b9d1401b48b5ea0405046200465b13c5873..640b56f1f02fd01759f4870f8d2a69b4b93b9ede 100644 (file)
--- 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 *)