-
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