aboutsummaryrefslogtreecommitdiff
path: root/tactics/pfedit.ml
AgeCommit message (Expand)Author
2019-10-09Specialize UState.merge for extend:falseGaëtan Gilbert
2019-10-09Simplify universe handling wrt side effects: rm demote_seff_univsGaëtan Gilbert
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on top...Emilio Jesus Gallego Arias