GitLab

We need to stop the transformation intro_premises to introduce variables
past a label. This allows us to keep variables in the goal (for counterex
generation) and be able to retrieve them as counterexamples.

* transform/intro_vc_vars_counterexmp.ml:
  changed vc_term_info so that it is not mutable anymore
  (do_intro): Removing the passing records to the do_intros calls which
may prevent us from seeing last vc_model
  (do_intro_vc_vars): adding a reference to keep the location of the vc

* transform/introduction.ml
  (intros): When encountering stop_intro label, the function should
stop introducing.

  added in 9577acb9

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

Since this might break some cases relying on opaqueness of
type variables occuring only in return types, opaqueness
annotations are now allowed there as well.

The goal is that most recent rules will shadow older ones.
Previous behavior was the converse.

When sessions are saved and then loaded from disk, goal identifiers are
properly qualified. This is not the case when goals are still in memory
due to reloading a file in the ide. So merging can get confused since
several goals potentially share the same base name.

The date at which the configure script was run does not carry much
information, so get rid of it.