]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/coq-contribs/LAMBDA-TYPES/cpr0_defs.v
ocaml 3.09 transition
[helm.git] / helm / coq-contribs / LAMBDA-TYPES / cpr0_defs.v
index 5434debd467a03b929b9e2033d65d99e5a84ea78..7773a3410ced2759291a097635e787ed113ad5d2 100644 (file)
@@ -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 *)