| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | more verbose logs for coq-makefile |  Enrico Tassi | 2017-07-20 |
| * | coq-makefile: quote using ' to preserve \ (windows paths) | Enrico Tassi | 2017-07-20 |
| * | coq-makefile: make test suite detect more errors | Enrico Tassi | 2017-07-20 |
| * | In fake_ide, call coqtop.exe instead of coqtop on Win32. |  Maxime Dénès | 2017-07-20 |
| * | Avoid using unsupported signals under Windows in fake_ide. | Maxime Dénès | 2017-07-20 |
| * | Remove trailing CR before diff in output and misc tests. | Maxime Dénès | 2017-07-20 |
| * | Print failure logs on appveyor. | Maxime Dénès | 2017-07-20 |
| * | Remove non-terminating Timeout tests from Hints.v. | Maxime Dénès | 2017-07-20 |
| * | Make coqlib relative in test suite (revert 024a7ab20b0) | Maxime Dénès | 2017-07-20 |
| * | Add AppVeyor infrastructure, launching the test suite under Windows. | Maxime Dénès | 2017-07-20 |
| * | Merge PR #900: [proofs] Remove circular dependency from Proofview to Goal. | Maxime Dénès | 2017-07-20 |
| |\ | |||
| * \ | Merge PR #899: [general] Move files to directories so they match linking order. | Maxime Dénès | 2017-07-20 |
| |\ \ | |||
| * \ \ | Merge PR #903: Documenting the purity / marshallability invariant of persiste... | Maxime Dénès | 2017-07-20 |
| |\ \ \ | |||
| | * | | | Documenting the purity / marshallability invariant of persistent states. |  Pierre-Marie Pédrot | 2017-07-20 |
| * | | | | Merge PR #898: [pp] Fix bugs 5651 [incorrect thunk in pretty printer] | Maxime Dénès | 2017-07-20 |
| |\ \ \ \ | |||
| * \ \ \ \ | Merge PR #896: Prepare De Bruijn universe abstractions, Spin-off: Checker | Maxime Dénès | 2017-07-20 |
| |\ \ \ \ \ | |||
| * \ \ \ \ \ | Merge PR #869: Enforce alternating separators in typeclass debug output | Maxime Dénès | 2017-07-20 |
| |\ \ \ \ \ \ | |||
| * \ \ \ \ \ \ | Merge PR #877: Travis+4.05.0 | Maxime Dénès | 2017-07-20 |
| |\ \ \ \ \ \ \ | |_|_|_|/ / / |/| | | | | | | |||
| * | | | | | | | Merge branch 'v8.7' | Maxime Dénès | 2017-07-20 |
| |\ \ \ \ \ \ \ | |||
| | * \ \ \ \ \ \ | Merge PR #745: Add timing scripts | Maxime Dénès | 2017-07-19 |
| | |\ \ \ \ \ \ \ | |||
| | * \ \ \ \ \ \ \ | Merge PR #855: Deprecate options that were introduced for compatibility with ... | Maxime Dénès | 2017-07-19 |
| | |\ \ \ \ \ \ \ \ | |||
| * | \ \ \ \ \ \ \ \ | Merge PR #770: [proof] Move bullets to their own module. | Maxime Dénès | 2017-07-19 |
| |\ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | * | [proofs] Remove circular dependency from Proofview to Goal. |  Emilio Jesus Gallego Arias | 2017-07-19 |
| | |_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | |||
| | | | | | | | | | * | [general] Move files to directories matching linking order. | Emilio Jesus Gallego Arias | 2017-07-19 |
| | |_|_|_|_|_|_|_|/ |/| | | | | | | | | |||
| * | | | | | | | | | Merge PR #788: [API] Remove `open API` in ml files in favor of `-open API` flag. | Maxime Dénès | 2017-07-19 |
| |\ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | * | [pp] Fix bugs 5651 [incorrect thunk in pretty printer] | Emilio Jesus Gallego Arias | 2017-07-19 |
| | |_|_|_|_|_|_|_|/ |/| | | | | | | | | |||
| | | | | | | | | * | Fixing the checker w.r.t. wrongly used abstract universe contexts. | Pierre-Marie Pédrot | 2017-07-19 |
| * | | | | | | | | | Merge PR #895: [ci] VST is now built with IGNORECOQVERSION=true. | Maxime Dénès | 2017-07-19 |
| |\ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ |/| | | | | | | | | |||
| | * | | | | | | | | [ci] VST is now built with IGNORECOQVERSION=true. |  Théo Zimmermann | 2017-07-18 |
| |/ / / / / / / / | |||
| * | | | | | | | | Merge PR #781: Remove dead code [Universes.simplify_universe_context] | Maxime Dénès | 2017-07-17 |
| |\ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ | Merge PR #783: Remove some useless code in Term_typing | Maxime Dénès | 2017-07-17 |
| |\ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ | Merge PR #822: [meta] [api] Fix META file for API introduction. | Maxime Dénès | 2017-07-17 |
| |\ \ \ \ \ \ \ \ \ \ | |||
| | | | | * | | | | | | | [funind] Remove spurious character in comment. | Emilio Jesus Gallego Arias | 2017-07-17 |
| | | | | * | | | | | | | [API] Remove `open API` in ml files in favor of `-open API` flag. | Emilio Jesus Gallego Arias | 2017-07-17 |
| | | | | * | | | | | | | [meta] [api] Fix META file for API introduction. | Emilio Jesus Gallego Arias | 2017-07-17 |
| | |_|_|/ / / / / / / |/| | | | | | | | | | |||
| * | | | | | | | | | | Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers | Maxime Dénès | 2017-07-17 |
| |\ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR #881: Adapting base_include to 91df40272 (body_of_constant_body move... | Maxime Dénès | 2017-07-17 |
| |\ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #879: Adding debug printers related to universes | Maxime Dénès | 2017-07-17 |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #874: Adding econstr printer to "include" file. | Maxime Dénès | 2017-07-17 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #872: [travis] Display info on tested commit for PR builds. | Maxime Dénès | 2017-07-17 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #865: RefMan-ext: fix some typos | Maxime Dénès | 2017-07-17 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #862: Adding support for bindings tags to explicit prefix/suffix rat... | Maxime Dénès | 2017-07-17 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | | * \ \ \ \ | Merge PR #861: Fix typo in documentation for identity | Maxime Dénès | 2017-07-17 |
| | | | | | | | | | | | | |\ \ \ \ \ | |||
| | | | | | | * | | | | | | | | | | | | Adapting to 91df40272 (body_of_constant_body moved to global). |  Hugo Herbelin | 2017-07-16 |
| | |_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | |||
| | | * | | | | | | | | | | | | | | | Update with non structurally recursive |  william-lawvere | 2017-07-14 |
| | | | | | * | | | | | | | | | | | | Adding debug printers related to universes in the default debugger source file. | Pierre-Marie Pédrot | 2017-07-14 |
| | |_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | |||
| | | | | | * | | | | | | | | | | | Fix a typo in dev/changes. | Pierre-Marie Pédrot | 2017-07-14 |
| | | | | | * | | | | | | | | | | | Document the changes in API brought by this series of patches. | Pierre-Marie Pédrot | 2017-07-14 |
| | | | | | * | | | | | | | | | | | Getting rid of abstraction breaking code in tclABSTRACT. | Pierre-Marie Pédrot | 2017-07-14 |
| | | | | | | | | | | | | | | * | | [travis] Update testing to 4.05.0 + Camlp5 7.01 | Emilio Jesus Gallego Arias | 2017-07-13 |
| | |_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |