Mentions légales du service

Skip to content
  • Andrei Paskevich's avatar
    - minor bugfix in Pretty · 988f29da
    Andrei Paskevich authored
    - move redefinition of f_app higher in Term
      to make sure that ps_neq can never appear
    - if a user "instantiates" a lemma as a goal on cloning, 
      the lemma just disappears (as it is alredy proved)
    - catch Not_found in merge_namespace on cloning,
      due to local goals not being cloned
    988f29da