| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-04 | Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`. | Maxime Dénès | |
| 2018-03-04 | Merge PR #6876: Unify Const_sorts and Const_type, and remove Vsort | Maxime Dénès | |
| 2018-03-04 | Merge PR #6873: [toplevel] Update state when `Drop` exception is thrown [#6872] | Maxime Dénès | |
| 2018-03-04 | Merge PR #6676: [proofview] goals come with a state | Maxime Dénès | |
| 2018-03-02 | [VM] Unify Const_sorts and Const_type, and remove Vsort. | Maxime Dénès | |
| This simplifies the representation of values, and brings it closer to the ones of the native compiler. | |||
| 2018-02-28 | [toplevel] Update state when `Drop` exception is thrown [#6872] | Emilio Jesus Gallego Arias | |
| `Drop` is implemented using exceptions-as-control flow, so the toplevel state gets corrupted as `do_vernac` will never return when `Drop` occurs in the input. The right fix would be to remove `Drop` from the vernacular and make it a toplevel-only command, but meanwhile we can just patch the state in the exception handler. We also need to keep the global state in `Coqloop` as the main `coqtop` entry point won't be called by `go ()`. Fixes #6872. | |||
| 2018-02-28 | [econstr] Continue consolidation of EConstr API under `interp`. | Emilio Jesus Gallego Arias | |
| This commit was motivated by true spurious conversions arising in my `to_constr` debug branch. The changes here need careful review as the tradeoffs are subtle and still a lot of clean up remains to be done in `vernac/*`. We have opted for penalize [minimally] the few users coming from true `Constr`-land, but I am sure we can tweak code in a much better way. In particular, it is not clear if internalization should take an `evar_map` even in the cases where it is not triggered, see the changes under `plugins` for a good example. Also, the new return type of `Pretyping.understand` should undergo careful review. We don't touch `Impargs` as it is not clear how to proceed, however, the current type of `compute_implicits_gen` looks very suspicious as it is called often with free evars. Some TODOs are: - impargs was calling whd_all, the Econstr equivalent can be either + Reductionops.whd_all [which does refolding and no sharing] + Reductionops.clos_whd_flags with all as a flag. | |||
| 2018-02-28 | Merge PR #6789: Check whitespace errors per-commit. | Maxime Dénès | |
| 2018-02-28 | Merge PR #6812: Rename release_lexer_state to the more descriptive ↵ | Maxime Dénès | |
| get_lexer_state. | |||
| 2018-02-24 | Merge PR #6543: Update headers and credits | Maxime Dénès | |
| 2018-02-24 | Merge PR #6803: coqdev.el: add space at the end of compile-command | Maxime Dénès | |
| 2018-02-23 | Check whitespace errors per-commit. | Gaëtan Gilbert | |
| Otherwise it is possible to detect errors that are not fixed by git rebase since that works per-commit. | |||
| 2018-02-22 | Tweak developer documentation. | Jim Fehrle | |
| 2018-02-22 | [ast] Improve precision of Ast location recognition in serialization. | Emilio Jesus Gallego Arias | |
| We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way. | |||
| 2018-02-21 | Merge PR #6767: [ci] add elpi | Maxime Dénès | |
| 2018-02-21 | Merge PR #6283: A pre-commit hook to magically fix whitespace issues. | Maxime Dénès | |
| 2018-02-21 | More accurate and complete headers. | Théo Zimmermann | |
| Remove the mention of specific labs (irrelevant for a copyright notice). Add a mention to represent other contributors and a pointer to CREDITS. | |||
| 2018-02-21 | coqdev.el: add space at the end of compile-command | Gaëtan Gilbert | |
| That way you can just type [-j] instead of having to remember to add a space yourself. | |||
| 2018-02-20 | overlay for ltac2 and Equations | Enrico Tassi | |
| 2018-02-19 | ci: add elpi | Enrico Tassi | |
| 2018-02-19 | Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t` | Maxime Dénès | |
| 2018-02-19 | Merge PR #6753: [toplevel] Make toplevel state into a record. | Maxime Dénès | |
| 2018-02-19 | Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵ | Maxime Dénès | |
| camlp4 | |||
| 2018-02-19 | Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead. | Maxime Dénès | |
| 2018-02-17 | Change references to CAMLP4 to CAMLP5 to be more accurate since we no | Jim Fehrle | |
| longer use camlp4. | |||
| 2018-02-15 | [toplevel] Make toplevel state into a record. | Emilio Jesus Gallego Arias | |
| We organize the toplevel execution as a record and pass it around. This will be used by future PRs as to for example decouple goal printing from the classifier. | |||
| 2018-02-13 | coqdev.el: wait for 'compile to touch compilation-error-regexp-alist | Gaëtan Gilbert | |
| (and alist-alist) | |||
| 2018-02-13 | coqdev.el: fix "compilate"-command typo | Gaëtan Gilbert | |
| 2018-02-13 | coqdev.el: shell-quote-argument the directory for make -C | Gaëtan Gilbert | |
| 2018-02-13 | coqdev.el: stop using when-let for emacs<25 compatibility. | Gaëtan Gilbert | |
| 2018-02-12 | [engine] Remove ghost parameter from `Proofview.Goal.t` | Emilio Jesus Gallego Arias | |
| In current code, `Proofview.Goal.t` uses a phantom type to indicate whether the goal was properly substituted wrt current `evar_map` or not. After the introduction of `EConstr`, this distinction should have become unnecessary, thus we remove the phantom parameter from `'a Proofview.Goal.t`. This may introduce some minor incompatibilities at the typing level. Code-wise, things should remain the same. We thus deprecate `assume`. In a next commit, we will remove normalization as much as possible from the code. | |||
| 2018-02-12 | Merge PR #6565: [Backport script] Check .mli files are not changed. | Maxime Dénès | |
| 2018-02-12 | Merge PR #6718: Fix redirection to stderr in lint-repository error message. | Maxime Dénès | |
| 2018-02-12 | Merge PR #6706: ci-common: guess CI_BRANCH for local builds | Maxime Dénès | |
| 2018-02-11 | Merge anomaly-traces-parser.el into coqdev.el. | Gaëtan Gilbert | |
| 2018-02-11 | coqdev.el: add installation instructions. | Gaëtan Gilbert | |
| 2018-02-08 | Fix redirection to stderr in lint-repository error message. | Gaëtan Gilbert | |
| 2018-02-08 | pre-commit: nicer messages | Gaëtan Gilbert | |
| 2018-02-08 | pre-commit: fail gracefully if fixing whitespace removes all changes | Gaëtan Gilbert | |
| 2018-02-08 | pre-commit: add files after fixing ending newlines. | Gaëtan Gilbert | |
| 2018-02-08 | Have the pre-commit hook also fix end-of-file nl | Jason Gross | |
| 2018-02-08 | Auto-create .git/hooks/pre-commit on ./configure | Jason Gross | |
| The hook created checks to see if dev/tools/pre-commit exists, and, if so, runs it. This way, we don't have to do any fancy logic to update the git pre-commit hook. The configure script never overwrites an existing precommit hook, so users can disable it by creating an empty pre-commit hook. The check for existence is so that if users check out an old version of Coq, attempting to commit won't give an error about non-existent files. | |||
| 2018-02-08 | pre-commit hook: fix whitespace error detection | Gaëtan Gilbert | |
| --quiet implies --exit-code | |||
| 2018-02-08 | A pre-commit hook to magically fix whitespace issues. | Gaëtan Gilbert | |
| 2018-02-07 | Merge PR #6610: Points to Flocq official repository. | Maxime Dénès | |
| 2018-02-07 | Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding | Maxime Dénès | |
| 2018-02-07 | ci-common: guess CI_BRANCH for local builds | Gaëtan Gilbert | |
| 2018-02-06 | Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document. | Maxime Dénès | |
| 2018-02-05 | Points to Flocq official repository. | Théo Zimmermann | |
| Following comment at https://github.com/coq/coq/pull/6596#issuecomment-358246528. | |||
| 2018-02-05 | Add overlay for equations (nf_beta takes an env) | Gaëtan Gilbert | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |