• MARCHE Claude's avatar
    Improved copy-paste functionality · a97edee6
    MARCHE Claude authored
    - copy from a transformation to a proof node works, adding
      the transformation below the target node
    
    - when copied transformation as less or more subgoals, then
      only the first subgoals are copied
    
    - explicit error message in case of invalid copy
    a97edee6
controller_itp.mli 12.7 KB