supported options of 'why3 session info: --stats, --graph, --provers
not supported: --tree, --edited-files, --dir

When Why3 is run on a file where some theories have been suppressed, it
will delete the corresponding theories from the session file.  We now
add an option keep_unmatched_theories to Session.update_session, which
keeps all theories. In this commit, this option is always disabled.

This is useful for SPARK, which sometimes only generates part of the
Why3 file for efficiency reasons, but doesn't want the session file to
be damaged because of that.

* session.ml
(import_theory)
(import_goal)
(import_proof_attempt)
(import_transf): new functions to copy a session tree from an old
  session file
(merge_file): keep old theories when keep_unmatched_theories is true
* session_scheduler.ml
(update_session): pass keep_unmatched_theories
* why3session_lib.ml
(read_update_session): pass keep_unmatched_theories

When resource limit is hit, cvc4 outputs useless counterexample. Query
cvc4 for the reason of answer unknown and use the answer to decide
whether resource limit was hit. If it was hit, do not display the
counterexample.

* src/driver/call_provers.{ml|mli}
(parse_prover_run): If the prover answers unknown, get the information
about the reason of this answer.

* src/printer/smtv2.ml
(print_prop_decl): Query solver for the reason of answer unknown.

* src/driver/driver.ml
(load_driver): Initialize Unknown with no information about the reason
of answer unknown.

* src/session/session.ml
(load_result): Initialize Unknown with no information about the reason
of answer unknown.

* src/session/session_scheduler.ml
(schedule_proof_attempt)
(edit_proof): Initialize Unknown with no information about the reason
of answer unknown.

* src/why3session/why3session_lib.ml
(filter_spec): Initialize Unknown with no information about the reason
of answer unknown.

              when one of the field is empty.

              (Thx Jean-Christophe)

(no yet displayed in IDE)

new goals are associated to old goals directly in the order they appear.
they are all marked obsolete, unless the theory itself is found non
obsolete (thanks to the new checksums for theories)

in other words, reloading a session on a file that did not change results
in non-obsolete goals, even if checksums and shapes are absent (e.g. if
the file was not put under version control)

and merge the why3 and why3session libraries back into one.

- make Whyconf.Args.initialize return the base config file, too.
  This is needed when we change configuration and want to save it.
- make Main pass "why3 <command>" as argv[0]
- remove "-version" options from everything but the main executable

two parts: why3 and why3session.

(The Coq tactic does not include why3session)

              rename options of why3session csv

	Just a proposition for a more controllable why3replayer

can be used with the task in a session

+ rename Debug.Opt to Debug.Args to avoid conflicts

+ create AUTHORS file
+ fix the linking exception in LICENSE
+ update the "About" in IDE
+ remove the trailing whitespace
+ inflate my scores at Ohloh

       Remove the id in prover that is used only for command-line, use
       instead the name,version,alternative of the prover. One can
       also use regular expression (start with ^).

       "Alt-Ergo,0.92,with arrays" corresponds only to one prover
       "Alt-Ergo,^0\.9.*,with arrays" correspond to all the Alt-Ergo prover with arrays which version match "0\.9.*"
       "Alt-Ergo" is the same thing than "Alt-Ergo,^,^"
       "Alt-Ergo,0.92," corresponds only to one prover with the alternate fields empty
       "Alt-Ergo,,with arrays" corresponds to "Alt-Ergo,^,with arrays" since the version is never empty.

       Provers identification are case sensitive even if it is
       currently more complicated for the user because
       case-insensitiveness is not sufficient. Specifiying "alt-ergo"
       for "Alt-Ergo,^,^" is great, but not if there is more than one
       match. A more general system of shortcut would be more
       appropriate.