aboutsummaryrefslogtreecommitdiff
path: root/theories/micromega/Tauto.v
AgeCommit message (Expand)Author
2020-12-15Catch up to where I was last time.Jasper Hugunin
2020-11-18[micromega] Optimised cnf in case an hypothesis is trivially False.BESSON Frederic
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-10-11Modify micromega/Tauto.v to compile with -mangle-namesJasper Hugunin
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
2020-04-01[micromega] use Coqlib.lib_ref to get Coq constants.Frédéric Besson
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias