| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-05-22 | Merge PR #7324: Infrastructure for ocamldebug on the checker | Hugo Herbelin | |
| 2018-05-22 | Merge PR #7526: [circle] Use Docker image from Gitlab registry. | Gaëtan Gilbert | |
| 2018-05-22 | Merge PR #7568: [ci] [gitlab] Fix printenv sorting for variables that span ↵ | Gaëtan Gilbert | |
| multiple lines | |||
| 2018-05-22 | [build] Add -cclib -lcoqrun options to build of kernel.cmxa. | Emilio Jesus Gallego Arias | |
| It seems that it is standard practice in the OCaml world to set the `-cclib` flags at library creation time, at least in native libraries. Indeed, this seems to make linking easier as seen for example in #7563. | |||
| 2018-05-22 | Merge PR #6859: [stm] Make toplevels standalone executables. | Théo Zimmermann | |
| 2018-05-21 | Simplify the newring hack. | Pierre-Marie Pédrot | |
| The new implementation is 100% compatible with the previous one, but it is more compact and does not use a tricky translation function from the kernel. | |||
| 2018-05-21 | [ci] [gitlab] Fix printenv sorting for variables that span multiple lines. | Emilio Jesus Gallego Arias | |
| 2018-05-21 | Fix an anomaly when calling Obligation 0 or Obligation -1. | Théo Zimmermann | |
| I didn't change the parser which expects an integer instead of a positive number because changing it would also mean having worse error messages because of our current LL parser. The error message would have been: Syntax error: 'Tactic' ':=' expected after 'Obligation' (in [vernac:command]). | |||
| 2018-05-21 | Remove a dead old-refman file. | Théo Zimmermann | |
| 2018-05-21 | Document the new nested-proof error message. | Théo Zimmermann | |
| 2018-05-21 | [ide] Remove special option `-ideslave` | Emilio Jesus Gallego Arias | |
| This has no effect anymore, verbose printing is controlled now by the regular, common `quiet` flag. | |||
| 2018-05-21 | [stm] Make toplevels standalone executables. | Emilio Jesus Gallego Arias | |
| We turn coqtop "plugins" into standalone executables, which will be installed in `COQBIN` and located using the standard `PATH` mechanism. Using dynamic linking for `coqtop` customization didn't make a lot of sense, given that only one of such "plugins" could be loaded at a time. This cleans up some code and solves two problems: - `coqtop` needing to locate plugins, - dependency issues as plugins in `stm` depended on files in `toplevel`. In order to implement this, we do some minor cleanup of the toplevel API, making it functional, and implement uniform build rules. In particular: - `stm` and `toplevel` have become library-only directories, - a new directory, `topbin`, contains the new executables, - 4 new binaries have been introduced, for coqide and the stm. - we provide a common and cleaned up way to locate toplevels. | |||
| 2018-05-21 | [ci] Add Dune to the base system. | Emilio Jesus Gallego Arias | |
| It is needed by Elpi and pidetop, and it is anyways needed for most OCaml packages, including some Coq tools in the future. The future base Docker image will include it by default. | |||
| 2018-05-20 | Maitainers for components of the test-suite (closes #7426). | Théo Zimmermann | |
| [ci skip] | |||
| 2018-05-20 | [codeowner] Add comment. | Théo Zimmermann | |
| [ci skip] | |||
| 2018-05-20 | Make Pierre-Marie a secondary maintainer of the kernel and checker. | Théo Zimmermann | |
| [ci skip] | |||
| 2018-05-20 | Merge PR #7557: Add test cases from #7554 | Théo Zimmermann | |
| 2018-05-20 | Add test cases from #7554 | Tej Chajed | |
| Failed in v8.7.2 but were fixed by v8.8.0. | |||
| 2018-05-19 | Merge PR #7527: [windows] Don't build menhir and int anymore in the ↵ | Michael Soegtrop | |
| packaging scripts. | |||
| 2018-05-18 | Merge PR #7550: [CI] Fix the script used by math-classes. | Emilio Jesus Gallego Arias | |
| 2018-05-18 | Fix #7539: Checker does not properly handle negative coinductive types. | Pierre-Marie Pédrot | |
| The reduction machine of the checker was not taking into account the fact that cofixpoints needed to be unfolded when applied against a projection. | |||
| 2018-05-18 | Merge PR #6965: [api] Move universe syntax to `Glob_term` | Pierre-Marie Pédrot | |
| 2018-05-18 | Clean-up dead file in test-suite. | Théo Zimmermann | |
| 2018-05-18 | Create a documentation for the release manager. | Théo Zimmermann | |
| This process is expected to evolve in the future as we automate it more and more. [ci skip] | |||
| 2018-05-18 | [CI] Fix the script used by math-classes. | Pierre-Marie Pédrot | |
| We call configure to properly regenerate the Makefile and its dependencies. | |||
| 2018-05-17 | Merge pull request #5 from gares/fix/tuto2 | Yves Bertot | |
| [tuto2] Clarify where the name of the ML plugin is used | |||
| 2018-05-17 | Merge pull request #4 from gares/fix/tuto0 | Yves Bertot | |
| fix plugin name in tuto0 | |||
| 2018-05-17 | Merge pull request #3 from gares/patch-1 | Yves Bertot | |
| Add some setup instructions | |||
| 2018-05-17 | Split off Universes functions for minimization. | Gaëtan Gilbert | |
| This finishes the splitting of Universes. | |||
| 2018-05-17 | Make Universes.refresh_constraints internal to UState | Gaëtan Gilbert | |
| 2018-05-17 | Split off Universes functions about substitutions and constraints | Gaëtan Gilbert | |
| 2018-05-17 | Remove unused argument to solve_constraints_system | Gaëtan Gilbert | |
| 2018-05-17 | Move solve_constraint_system near its only use site (comInductive) | Gaëtan Gilbert | |
| 2018-05-17 | Split off Universes functions dealing with generating new universes. | Gaëtan Gilbert | |
| 2018-05-17 | Split off Universes functions dealing with names. | Gaëtan Gilbert | |
| This API is a bit strange, I expect it will change at some point. | |||
| 2018-05-17 | Stop using Universes.subst(_opt)_univs_constr | Gaëtan Gilbert | |
| Should it be removed? The underlying `universe_subst -> constr -> constr` seems like it could be useful for plugins but where would the substitution be from? | |||
| 2018-05-17 | Make set minimization option internal to Universes | Gaëtan Gilbert | |
| 2018-05-17 | [circle] Use Docker image from Gitlab registry. | Emilio Jesus Gallego Arias | |
| 2018-05-17 | Merge PR #7451: Introduce an option to allow nested lemma, and turn it off ↵ | Emilio Jesus Gallego Arias | |
| by default. | |||
| 2018-05-17 | Merge PR #7359: Reduce usage of evar_map references | Pierre-Marie Pédrot | |
| 2018-05-17 | [tuto2] Clarify where the name of the ML plugin is used | Enrico Tassi | |
| 2018-05-17 | add little test | Enrico Tassi | |
| - tests the plugin can actually be loaded (eg with the wrong DECLARE PLUGIN it loads but then the tactic is not in scope) - sine is listed in _CoqProject one can open it with CoqIDE/PG and get the -I -R flags from the _CoqProject automatically | |||
| 2018-05-17 | DECLARE PLUGIN "$name" === Declare ML Module "$name" | Enrico Tassi | |
| 2018-05-17 | Add some setup instructions | Enrico | |
| 2018-05-17 | Merge pull request #2 from gares/gares-patch-1 | Yves Bertot | |
| [tuto1] Minor fixes to comments | |||
| 2018-05-17 | [tuto1] Minor fixes to comments | Enrico | |
| 2018-05-17 | Merge PR #7449: [vernac] taint two out-of-api `to_constr` use in ↵ | Pierre-Marie Pédrot | |
| `comDefinition`. | |||
| 2018-05-17 | Merge PR #6870: [ide] Don't set `quiet` on start. | Enrico Tassi | |
| 2018-05-17 | Merge PR #7525: [ci] Try to build more of fiat-crypto. | Gaëtan Gilbert | |
| 2018-05-17 | Merge PR #6808: Add unit tests to test-suite | Gaëtan Gilbert | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |