Commit 16d53dd2 authored by Armaël Guéneau's avatar Armaël Guéneau

Fix a deprecation warning wrt Zmax & Zmin under coq 8.8

parent 9a0583c7
......@@ -349,8 +349,8 @@ let inlined_primitives_table =
"Pervasives.<=", (Primitive_binary_only_numbers, "(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.le _ TLC.LibInt.le_int_inst x__ y__))");
"Pervasives.>", (Primitive_binary_only_numbers, "(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.gt _ (@TLC.LibOrder.gt_of_le _ TLC.LibInt.le_int_inst) x__ y__))");
"Pervasives.>=", (Primitive_binary_only_numbers, "(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.ge _ (@TLC.LibOrder.ge_of_le _ TLC.LibInt.le_int_inst) x__ y__))");
"Pervasives.max", (Primitive_binary_only_numbers, "Coq.ZArith.BinInt.Zmax");
"Pervasives.min", (Primitive_binary_only_numbers, "Coq.ZArith.BinInt.Zmin");
"Pervasives.max", (Primitive_binary_only_numbers, "Coq.ZArith.BinInt.Z.max");
"Pervasives.min", (Primitive_binary_only_numbers, "Coq.ZArith.BinInt.Z.min");
"List.length", (Primitive_unary, "(@TLC.LibListZ.length _)");
"List.rev", (Primitive_unary, "(@TLC.LibList.rev _)");
"List.concat", (Primitive_unary, "(@TLC.LibList.concat _)");
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment