ocaml 3.09 transition

[helm.git] / helm / matita / contribs / LAMBDA-TYPES / lref_map_defs.ma

diff --git a/helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma
index f2994f9b79b5185b4250e5ff11bc5956b703fbf0..572618808d33101ac9bbcd6e1de7c45c533009e8 100644 (file)
--- a/helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma
+++ b/helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma
@@ -18,5 +18,5 @@ include "terms_defs.ma".
 
 inductive tlref_map (A: Set) (N: Set) (map: nat \to nat): nat \to (T A N) \to (T A N) \to Prop \def
    | tlref_map_sort: \forall i. \forall k. \forall y. (tlref_map A N map i (TSort A N y k) (TSort A N y k))
-   | tlref_map_lref_lt: \forall j. \forall i. \forall y. (lt j i) \to (tlref_map A N map i (TLRef A N y j) (TLRef A N y j))
-   | tlref_map_lref_ge: \forall j. \forall i. \forall y. (le i j) \to (tlref_map A N map i (TLRef A N y j) (TLRef A N y (map j))).
\ No newline at end of file
+   | tlref_map_lref_lt: \forall j. \forall i. \forall y. j < i \to (tlref_map A N map i (TLRef A N y j) (TLRef A N y j))
+   | tlref_map_lref_ge: \forall j. \forall i. \forall y. i \le j \to (tlref_map A N map i (TLRef A N y j) (TLRef A N y (map j))).