aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Expand)AuthorAge
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25
* Add AppVeyor infrastructure, launching the test suite under Windows.Gravatar Maxime Dénès2017-07-20
* Merge PR #788: [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Maxime Dénès2017-07-19
|\
* | [ci] VST is now built with IGNORECOQVERSION=true.Gravatar Théo Zimmermann2017-07-18
| * [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
|/
* Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layersGravatar Maxime Dénès2017-07-17
|\
* \ Merge PR #881: Adapting base_include to 91df40272 (body_of_constant_body move...Gravatar Maxime Dénès2017-07-17
|\ \
* \ \ Merge PR #879: Adding debug printers related to universesGravatar Maxime Dénès2017-07-17
|\ \ \
| | * | Adapting to 91df40272 (body_of_constant_body moved to global).Gravatar Hugo Herbelin2017-07-16
| * | | Adding debug printers related to universes in the default debugger source file.Gravatar Pierre-Marie Pédrot2017-07-14
| |/ /
| | * Fix a typo in dev/changes.Gravatar Pierre-Marie Pédrot2017-07-14
| | * Document the changes in API brought by this series of patches.Gravatar Pierre-Marie Pédrot2017-07-14
| |/
* / Adding econstr printer to "include" file.Gravatar Hugo Herbelin2017-07-12
|/
* Merge PR #858: [travis] Remove CompCert version check hack.Gravatar Maxime Dénès2017-07-11
|\
| * [travis] Remove CompCert version check hack.Gravatar Emilio Jesus Gallego Arias2017-07-05
* | Revert fiat-crypto overlayGravatar Jason Gross2017-07-04
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| * Fix libpcre dependency issue under Windows.Gravatar Maxime Dénès2017-06-26
| * Fix proxy setting issueGravatar Michael Soegtrop2017-06-26
| * Fixes bug #5561,#5562 in Windows build systemGravatar Michael Soegtrop2017-06-26
* | Add missing definition and fix #use include;; as suggested by @amintimany.Gravatar Théo Zimmermann2017-06-22
* | Merge PR#774: [ide] Add route_id parameter to query call.Gravatar Maxime Dénès2017-06-20
|\ \
* \ \ Merge PR#779: Each user overlay goes into its own file.Gravatar Maxime Dénès2017-06-20
|\ \ \
| | * | [ide] Add route_id parameter to query call.Gravatar Emilio Jesus Gallego Arias2017-06-18
| | | * Remove -j ${NJOBS} from make invocations in the ciGravatar Jason Gross2017-06-16
| | | * Fix ci-fiat-crypto to have a proper lite targetGravatar Jason Gross2017-06-16
| * | | Each user overlay goes into its own file.Gravatar Théo Zimmermann2017-06-16
* | | | Fix a bug in cumulativityGravatar Amin Timany2017-06-16
* | | | A short cleanupGravatar Amin Timany2017-06-16
* | | | Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* | | | Squashed commit of the following:Gravatar Amin Timany2017-06-16
| |/ / |/| |
* | | Merge PR#778: Revert "[travis] temporary UniMath overlay"Gravatar Maxime Dénès2017-06-15
|\ \ \
* | | | fix dev/base_include (thanks Zimmi48)Gravatar Pierre Letouzey2017-06-15
* | | | Remove bedrock from test suite.Gravatar Maxime Dénès2017-06-15
| |/ / |/| |
* | | Merge PR#749: Normalize deprecation notices of ./configureGravatar Maxime Dénès2017-06-14
|\ \ \
* \ \ \ Merge PR#622: Change the default flag value for Refine.refineGravatar Maxime Dénès2017-06-14
|\ \ \ \
* \ \ \ \ Merge PR#771: [travis overlay] Partially Revert 013c0232953f1f58Gravatar Maxime Dénès2017-06-14
|\ \ \ \ \
* | | | | | Temporary overlays because fewer plugins are loaded at startup.Gravatar Maxime Dénès2017-06-14
* | | | | | [travis] overlay for fiat-crypto (a Require Import FunInd)Gravatar Pierre Letouzey2017-06-14
* | | | | | [travis] overlays for CompCert and VST (an extra Require Export FunInd)Gravatar Pierre Letouzey2017-06-14
* | | | | | [travis] fix Software Foundation (one added Require Extraction)Gravatar Pierre Letouzey2017-06-14
* | | | | | [travis] fix CoLoR by inserting some Require Import FunIndGravatar Pierre Letouzey2017-06-14
* | | | | | Temporary overlays for bignums.Gravatar Maxime Dénès2017-06-14
* | | | | | Merge PR#498: Bignums as a separate opam packageGravatar Maxime Dénès2017-06-14
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#766: Fix ocamldebug for the APIGravatar Maxime Dénès2017-06-13
|\ \ \ \ \ \ \
| | | | | | * | Revert "[travis] temporary UniMath overlay"Gravatar Théo Zimmermann2017-06-13
| |_|_|_|_|/ / |/| | | | | |
* | | | | | | Merge PR#714: Print feature Proof-of-Concept (episode 2)Gravatar Maxime Dénès2017-06-13
|\ \ \ \ \ \ \
| | | | | * | | Dualize the unsafe flag of refine into typecheck and make it mandatory.Gravatar Pierre-Marie Pédrot2017-06-13