aboutsummaryrefslogtreecommitdiffstats
path: root/common/Linking.v
Commit message (Expand)AuthorAgeFilesLines
* Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-031-10/+10
* Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-151-1/+1
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-1/+1
* Use `Program Instance` instead of `Instance` + refine mode (#261)Maxime Dénès2018-12-271-41/+53
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-63/+63
* The basic framework for linking and separate compilation.Xavier Leroy2016-03-061-0/+905