| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-10 | [ssreflect] Fix module scoping problems due to packing and mli files. | Emilio Jesus Gallego Arias | |
| Unfortunately, mli-only files cannot be included in packs, so we have the weird situation that the scope for `Tacexpr` is wrong. So we cannot address the module as `Ltac_plugin.Tacexpr` but it lives in the global namespace instead. This creates problem when using other modular build/packing strategies [such as #6857] This could be indeed considered a bug in the OCaml compiler. In order to remedy this situation we face two choices: - leave the module out of the pack (!) - create an implementation for the module I chose the second solution as it seems to me like the most sensible choice. cc: #6512. | |||
| 2018-03-09 | [located] Push inner locations in `reference` to a CAst.t node. | Emilio Jesus Gallego Arias | |
| The `reference` type contains some ad-hoc locations in its constructors, but there is no reason not to handle them with the standard attribute container provided by `CAst.t`. An orthogonal topic to this commit is whether the `reference` type should contain a location or not at all. It seems that many places would become a bit clearer by splitting `reference` into non-located `reference` and `lreference`, however some other places become messier so we maintain the current status-quo for now. | |||
| 2018-03-09 | [located] More work towards using CAst.t | Emilio Jesus Gallego Arias | |
| We continue with the work of #402 and #6745 and update most of the remaining parts of the AST: - module declarations - intro patterns - top-level sentences Now, parsed documents should be full annotated by `CAst` nodes. | |||
| 2018-03-09 | Merge PR #6775: Allow using cumulativity without forcing strict constraints. | Maxime Dénès | |
| 2018-03-09 | Overlay for Elpi. | Gaëtan Gilbert | |
| 2018-03-09 | Add an overlay for Equations and Ltac2. | Pierre-Marie Pédrot | |
| 2018-03-08 | Merge PR #6817: [configure]: support for profiles | Maxime Dénès | |
| 2018-03-08 | Merge PR #6881: [windows] support -addon in build script | Maxime Dénès | |
| 2018-03-06 | document -profile in dev/doc/setup.txt | Enrico Tassi | |
| 2018-03-06 | Standard headers for C and Python. | Maxime Dénès | |
| 2018-03-06 | Hack to make bignum build on windows | Enrico Tassi | |
| 2018-03-06 | build: win: turn off build/installation of gnu Make | Enrico Tassi | |
| 2018-03-05 | Merge PR #6855: Update headers following #6543. | Maxime Dénès | |
| 2018-03-04 | Merge PR #935: Handling evars in the VM | Maxime Dénès | |
| 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-03 | Handling evars in the VM. | Pierre-Marie Pédrot | |
| We simply treat them as as an application of an atom to its instance, and in the decompilation phase we reconstruct the instance from the stack. This grants wish BZ#5659. | |||
| 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-03-02 | installer: win: put addons in a separate package | Enrico Tassi | |
| 2018-03-02 | build: win: detect 404 as HTML files | Enrico Tassi | |
| 2018-03-02 | build: win: addon bignums | Enrico Tassi | |
| 2018-03-02 | build: win: support for addons | Enrico Tassi | |
| 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-27 | Update headers following #6543. | Théo Zimmermann | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |