Extend the tests:

1) Make sure that extraction to JSON fails
2) Make sure that extracting callbacks can be reverted.

test-suite/failure/extraction_ffi.v

@@ -21,7 +21,12 @@ Extraction Language Scheme.
 Fail Extract Foreign Constant ax_fun => "my_c_fun".
 Fail Extract Callback "call_my_fun" my_fun.
 
+(* Extraction of foreign constant and callback for JSON must fail *)
+Extraction Language JSON.
+Fail Extract Foreign Constant ax_fun => "my_c_fun".
+Fail Extract Callback "call_my_fun" my_fun.
+
 (* Extraction of foreign constant for already defined ml function must fail. *)
 Extraction Language OCaml.
 Extract Constant ax_fun => "my_ml_fun".
-Fail Extract Foreign Constant ax_fun => "my_c_fun".
+Fail Extract Foreign Constant ax_fun => "my_c_fun".

test-suite/output/Extraction_ffi.out

@@ -16,3 +16,7 @@ let exact_fun2 a =
   add (ax_fun a) (S O)
 
 let _ = Stdlib.Callback.register "call_exact_fun" exact_fun2
+(** val exact_fun2 : nat -> nat **)
+
+let exact_fun2 a =
+  add (ax_fun a) (S O)

test-suite/output/Extraction_ffi.v

@@ -22,6 +22,10 @@ Extraction exact_fun.
 Extract Foreign Constant exact_fun => "my_exact_c_fun".
 Extraction exact_fun.
 
-(* Now, exact_fun is an entry point exposed to C. *)
+(* Now, exact_fun is an entry point exposed to C *)
 Extract Callback "call_exact_fun" exact_fun2.
 Extraction exact_fun2.
+
+(* Now we make sure that a callback registration can be reverted *)
+Reset Extraction Callback.
+Extraction exact_fun2.