-
Sylvain Dailler authored
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.
83b74fbd