aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/NoAxiomFromR.v
AgeCommit message (Expand)Author
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2019-09-09[stdlib] Do not put INR_eq in the “real” hint databaseVincent Laporte