Serious test for the Coq library added (name test_library).

Serious test for the Coq library added (name test_library).
Input: a file that holds a list of URIs.
Output: the benchmark; the output file is also a valid input.
        In this case the output also prints the differences w.r.t. the
        last execution.
Ctrl-break can be used to interrupt the type-checking of a single URI.
An interactive question is posed to the user to decide if proceeding with
the next URIs or not.