• Sylvain Dailler's avatar
    P718-014 Adding a label stop_intros into introduce_premises · 83b74fbd
    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
introduction.ml 3.2 KB