Sample fails within a module definition #369

The Sample command fails within a module definition. For example,

From QuickChick Require Import QuickChick.
Module M.
  Sample (returnGen 0).

yields an error

Error:
Could not compile test program: /var/folders/lg/gfn_5bmn2xs8ppvwp0wc4s0c0000gq/T/QuickChick/131734_5a4cfb/QuickChick991ac1.ml

Build stdout:
+ ocamlfind ocamlopt -c -w -3 -package zarith -o QuickChick991ac1.cmx QuickChick991ac1.ml
File "QuickChick991ac1.ml", line 200, characters 9-19:
200 | let l = (quickchick) in
               ^^^^^^^^^^
Error: Unbound value quickchick
Command exited with code 2.

The error is caused by the fact that the definition of module M is closed in the extracted program, which then calls the quickchick function defined in the module.
If the command call is prohibited within a module definition, I would expect to receive the same error as if I had called it within a section definition where

From QuickChick Require Import QuickChick.
Section S.
  Sample (returnGen 0).

yields an error

The command has indeed failed with message:
You can't do that within a section.
Close it and try again.

Of course, it would be also nice to solve this problem by allowing the command to be used without prohibiting it. In fact, in older versions of QuickChick, it was possible to call the Sample command even in module definitions.

However, this problem may not be solved in the QuickChick since the above error message (in the case of a section) seems to be output by the check_inside_section function in the extraction of Coq.