aboutsummaryrefslogtreecommitdiff
path: root/tactics/declareUctx.ml
AgeCommit message (Expand)Author
2020-12-02Stop calling Id.Map.domain on univ binders every individual universeGaëtan Gilbert
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-04-21[declare] [tactics] Move declare to `vernac`Emilio Jesus Gallego Arias