diff --git a/examples/sudoku/Makefile b/examples/sudoku/Makefile
index 0485c61ad9132b40494e56ca9c226b313c621edc..9347e2a797796f5f9246f13ad40f64a85bad6191 100644
--- a/examples/sudoku/Makefile
+++ b/examples/sudoku/Makefile
@@ -19,10 +19,12 @@ ifeq ($(BENCH),yes)
   INCLUDE += -I ../../lib/why3
 endif
 
-MAIN = main
-OBJ = map__Map sudoku__Grid sudoku__TheClassicalSudokuGrid sudoku__Solver
+MAIN=main
+GEN = map__Map sudoku__Grid sudoku__TheClassicalSudokuGrid sudoku__Solver
+OBJ=$(GEN)
 
-ML  = $(addsuffix .ml, $(OBJ))
+GENML = $(addsuffix .ml, $(GEN))
+ML = $(addsuffix .ml, $(OBJ))
 CMO = $(addsuffix .cmo, $(OBJ))
 CMX = $(addsuffix .cmx, $(OBJ))
 
@@ -30,7 +32,7 @@ OCAMLOPT = ocamlopt -noassert -inline 1000
 
 all: $(MAIN).opt
 
-extract: $(ML)
+extract: $(GENML)
 
 doc:
 	$(WHY3) doc ../sudoku.mlw
@@ -44,7 +46,7 @@ $(MAIN).opt: $(CMX) $(MAIN).cmx
 
 $(MAIN).cmx: $(CMX)
 
-$(ML): ../sudoku.mlw
+$(GENML): ../sudoku.mlw
 	$(WHY3) extract -D ocaml32 ../sudoku.mlw -o .
 
 # javascript
@@ -56,10 +58,10 @@ JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
           -syntax camlp4o
 
 $(JSMAIN).js: $(JSMAIN).byte
-	js_of_ocaml -pretty -noinline $(JSMAIN).byte
+	js_of_ocaml -pretty -noinline +nat.js $(JSMAIN).byte
 
-$(JSMAIN).byte: $(ML) $(JSMAIN).cmo
-	$(JSOCAMLC) -g -o $@ -linkpkg $^
+$(JSMAIN).byte: $(CMO) $(JSMAIN).cmo
+	$(JSOCAMLC) $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ -linkpkg $^
 
 %.cmo: %.ml
 	$(JSOCAMLC) $(INCLUDE) -annot -c $<
@@ -71,6 +73,6 @@ $(JSMAIN).byte: $(ML) $(JSMAIN).cmo
 	$(OCAMLOPT) $(INCLUDE) -annot -c $<
 
 clean::
-	rm -f $(ML) *.annot *.o *.cm[xio] $(MAIN).opt $(MAIN).byte
+	rm -f $(GENML) *.annot *.o *.cm[xio] $(MAIN).opt $(MAIN).byte
 	rm -f sudoku__*.ml why3__*.ml
 	rm -f int__Int.ml map__Map.ml array__Array.ml
diff --git a/examples/sudoku/jsmain.ml b/examples/sudoku/jsmain.ml
index adec3e3d9841d0b9376b5243a5334d5017e295b0..c16617e28c6d1ecfc015c4e839a64b5e5a296be1 100644
--- a/examples/sudoku/jsmain.ml
+++ b/examples/sudoku/jsmain.ml
@@ -1,4 +1,7 @@
 
+
+let () = Firebug.console##info (Js.string "debut de jsmain.ml")
+
 module D = Dom_html
 
 let d = D.document
@@ -201,10 +204,10 @@ let onload (_event : #Dom_html.event Js.t) : bool Js.t =
     (fun () -> assert false) in
   Dom.appendChild board table;
   board##style##backgroundColor <- Js.string "#00ff00";
-  board##style##paddingLeft <- Js.string "100px";
-  board##style##paddingRight <- Js.string "100px";
-  board##style##paddingBottom <- Js.string "100px";
-  board##style##paddingTop <- Js.string "100px";
+  board##style##paddingLeft <- Js.string "40px";
+  board##style##paddingRight <- Js.string "40px";
+  board##style##paddingBottom <- Js.string "40px";
+  board##style##paddingTop <- Js.string "40px";
   Js._false
 
 let _ = Dom_html.window##onload <- Dom_html.handler onload
diff --git a/examples/sudoku/main.ml b/examples/sudoku/main.ml
index dccc085923c5d9ba6f61480ccd8820ef78ec85a5..14ef3d5498ed27e5cc0a13ef37cab5e1c7eccacc 100644
--- a/examples/sudoku/main.ml
+++ b/examples/sudoku/main.ml
@@ -37,7 +37,7 @@ let print_grid fmt a =
 let () =
   let sudoku = Sudoku__TheClassicalSudokuGrid.classical_sudoku () in
   printf "Problem: %a@." print_grid input_grid;
-  let a = Sudoku__Solver.solve sudoku input_grid 
+  let a = Sudoku__Solver.solve sudoku input_grid
   in
   printf "Solution: %a@." print_grid a
 
@@ -46,6 +46,18 @@ test:
 
 2,0,9,0,0,0,0,1,0,0,0,0,0,6,0,0,0,0,0,5,3,8,0,2,7,0,0,3,0,0,0,0,0,0,0,0,0,0,0,0,7,5,0,0,3,0,4,1,2,0,8,9,0,0,0,0,4,0,9,0,0,2,0,8,0,0,0,0,1,0,0,5,0,0,0,0,0,0,0,7,6
 
+that is
+
+2 0 9 0 0 0 0 1 0
+0 0 0 0 6 0 0 0 0
+0 5 3 8 0 2 7 0 0
+3 0 0 0 0 0 0 0 0
+0 0 0 0 7 5 0 0 3
+0 4 1 2 0 8 9 0 0
+0 0 4 0 9 0 0 2 0
+8 0 0 0 0 1 0 0 5
+0 0 0 0 0 0 0 7 6
+
 should give:
 
 2 6 9 3 5 7 8 1 4
diff --git a/examples/vstte12_combinators/Makefile b/examples/vstte12_combinators/Makefile
index bc4b4bc041cf55d369cdebf81db09dbe4d902ec2..687be1fd17fea78e08d88810514a7cb219952522 100644
--- a/examples/vstte12_combinators/Makefile
+++ b/examples/vstte12_combinators/Makefile
@@ -62,12 +62,12 @@ JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
           -syntax camlp4o
 
 $(JSMAIN).js: $(JSMAIN).byte
-	js_of_ocaml -pretty -noinline $(JSMAIN).byte
+	js_of_ocaml -pretty -noinline +nat.js $(JSMAIN).byte
 
 
-$(JSMAIN).byte: $(ML) jsmain.ml
-	$(JSOCAMLC) $(INCLUDE) -o $@ -linkpkg $^
-#	$(JSOCAMLC) $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ -linkpkg $^
+$(JSMAIN).byte: $(CMO) jsmain.ml
+#	$(JSOCAMLC) $(INCLUDE) -o $@ -linkpkg $^
+	$(JSOCAMLC) $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ -linkpkg $^
 
 
 %.cmo: %.ml
diff --git a/examples/vstte12_combinators/jsmain.ml b/examples/vstte12_combinators/jsmain.ml
index f08855bfb2f283515de310eb41d9f526c6fec9a0..4e836ab7641b5ef434a7626dee0e14ba6594fc85 100644
--- a/examples/vstte12_combinators/jsmain.ml
+++ b/examples/vstte12_combinators/jsmain.ml
@@ -1,5 +1,8 @@
 
 
+
+let () = Firebug.console##info (Js.string "debut de jsmain.ml")
+
 (* computation part  *)
 
 let compute_result text =