aboutsummaryrefslogtreecommitdiffstats
path: root/common/Unityping.v
Commit message (Expand)AuthorAgeFilesLines
* [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-4/+5
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-3/+3
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-8/+8
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-3/+3
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-42/+42
* Merge of branch linear-typing:xleroy2014-04-061-0/+435
* Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping):xleroy2014-03-281-435/+0
* Revised division of labor between RTLtyping and Lineartyping:xleroy2014-03-271-0/+435