aboutsummaryrefslogtreecommitdiff
path: root/theories/extraction
AgeCommit message (Expand)Author
2021-03-28Replace mentions of Num by Zarith.Guillaume Melquiond
2021-02-26Signed primitive integersAna
2020-10-08Remove occurrences of Parray.reroot.Guillaume Melquiond
2020-07-06Primitive persistent arraysMaxime Dénès
2020-05-09Merge PR #12263: HaskellExtr: Add type annotations to Prelude.==Kazuhiko Sakaguchi
2020-05-08Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpointsPierre-Marie Pédrot
2020-05-06HaskellExtr: Add type annotations to Prelude.==Jason Gross
2020-05-01Fixing #11903: Fixpoints not truly recursive in standard library.Hugo Herbelin
2020-04-05Quoting _CoqProject in a comment to avoid coqdoc to interpret it as emphasis.Hugo Herbelin
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