stdlib: added witness, mach.matrix, mach.peano, and mach.onetime

to the HTML on-line version of the standard library

Makefile.in

@@ -2067,8 +2067,12 @@ STDLIBS = \
 	stack \
 	string \
 	sum \
+	witness \
         mach/array \
-	mach/int
+	mach/int \
+        mach/matrix \
+	mach/onetime \
+	mach/peano
 # function ? tptp ?
 
 STDLIBFILES = $(patsubst %,stdlib/%.mlw, $(STDLIBS))

stdlib/mach/int.mlw

 
-(** {1 Arithmetic for programs} *)
+(** {1 Machine Arithmetic} *)
 
 (** {2 Integer Division}
 

stdlib/mach/matrix.mlw

-(** {1 Matrices} *)
+(** {1 Matrices with bounded-size integers} *)
 
 module Matrix63
 

stdlib/mach/onetime.mlw

 
-(** {2 One-time integers} *)
+(** {2 One-time integers}
+
+  This module implements the idea described in this paper:
+  {h <a href="https://hal.inria.fr/hal-01162661">
+     How to avoid proving the absence of integer overflows</a>}
+
+  When extracted to OCaml, the following type `OneTime.t` will be mapped to
+  OCaml's type `int` (63-bit signed integers).
+
+  See also `mach.peano`.
+*)
 
 module OneTime
 

stdlib/mach/peano.mlw

 
-(** {2 Peano arithmetic} *)
+(** {2 Peano arithmetic}
+
+  This module implements the idea described in this paper:
+  {h <a href="https://hal.inria.fr/hal-01162661">
+     How to avoid proving the absence of integer overflows</a>}
+
+  When extracted to OCaml, the following type `Peano.t` will be mapped to
+  OCaml's type `int` (63-bit signed integers).
+
+  See also `mach.onetime`.
+*)
 
 module Peano