aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* \ Merge PR #935: Handling evars in the VMGravatar Maxime Dénès2018-03-04
|\ \
* \ \ Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Maxime Dénès2018-03-04
|\ \ \
* \ \ \ Merge PR #6876: Unify Const_sorts and Const_type, and remove VsortGravatar Maxime Dénès2018-03-04
|\ \ \ \
* \ \ \ \ Merge PR #6873: [toplevel] Update state when `Drop` exception is thrown [#6872]Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6676: [proofview] goals come with a stateGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \
| | | | | * | Handling evars in the VM.Gravatar Pierre-Marie Pédrot2018-03-03
| |_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | * | | [VM] Unify Const_sorts and Const_type, and remove Vsort.Gravatar Maxime Dénès2018-03-02
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | This simplifies the representation of values, and brings it closer to the ones of the native compiler.
| | * | | [toplevel] Update state when `Drop` exception is thrown [#6872]Gravatar Emilio Jesus Gallego Arias2018-02-28
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | `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.
| | * | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | Merge PR #6789: Check whitespace errors per-commit.Gravatar Maxime Dénès2018-02-28
|\ \ \
* \ \ \ Merge PR #6812: Rename release_lexer_state to the more descriptive ↵Gravatar Maxime Dénès2018-02-28
|\ \ \ \ | | | | | | | | | | | | | | | get_lexer_state.
| | | | * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |_|_|/ |/| | |
* | | | Merge PR #6543: Update headers and creditsGravatar Maxime Dénès2018-02-24
|\ \ \ \
* \ \ \ \ Merge PR #6803: coqdev.el: add space at the end of compile-commandGravatar Maxime Dénès2018-02-24
|\ \ \ \ \
| | | | * | Check whitespace errors per-commit.Gravatar Gaëtan Gilbert2018-02-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Otherwise it is possible to detect errors that are not fixed by git rebase since that works per-commit.
| | | * | | Tweak developer documentation.Gravatar Jim Fehrle2018-02-22
| | | |/ /
* | | | | [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | Merge PR #6767: [ci] add elpiGravatar Maxime Dénès2018-02-21
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6283: A pre-commit hook to magically fix whitespace issues.Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ | |_|_|_|/ / |/| | | | |
| | | | * | More accurate and complete headers.Gravatar Théo Zimmermann2018-02-21
| |_|_|/ / |/| | | | | | | | | | | | | | | | | | | Remove the mention of specific labs (irrelevant for a copyright notice). Add a mention to represent other contributors and a pointer to CREDITS.
| | | * | coqdev.el: add space at the end of compile-commandGravatar Gaëtan Gilbert2018-02-21
| |_|/ / |/| | | | | | | | | | | | | | | That way you can just type [-j] instead of having to remember to add a space yourself.
| | | * overlay for ltac2 and EquationsGravatar Enrico Tassi2018-02-20
| |_|/ |/| |
| | * ci: add elpiGravatar Enrico Tassi2018-02-19
| |/ |/|
* | Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Maxime Dénès2018-02-19
|\ \
* \ \ Merge PR #6753: [toplevel] Make toplevel state into a record.Gravatar Maxime Dénès2018-02-19
|\ \ \
* \ \ \ Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵Gravatar Maxime Dénès2018-02-19
|\ \ \ \ | | | | | | | | | | | | | | | camlp4
* \ \ \ \ Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.Gravatar Maxime Dénès2018-02-19
|\ \ \ \ \
| | * | | | Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | | | | | | | | | | | | | | | | | | | | | | | longer use camlp4.
| | | * | | [toplevel] Make toplevel state into a record.Gravatar Emilio Jesus Gallego Arias2018-02-15
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | | coqdev.el: wait for 'compile to touch compilation-error-regexp-alistGravatar Gaëtan Gilbert2018-02-13
| | | | | | | | | | | | | | | | | | | | (and alist-alist)
| * | | | coqdev.el: fix "compilate"-command typoGravatar Gaëtan Gilbert2018-02-13
| | | | |
| * | | | coqdev.el: shell-quote-argument the directory for make -CGravatar Gaëtan Gilbert2018-02-13
| | | | |
| * | | | coqdev.el: stop using when-let for emacs<25 compatibility.Gravatar Gaëtan Gilbert2018-02-13
| | | | |
| | | * | [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | Merge PR #6565: [Backport script] Check .mli files are not changed.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ | |_|_|/ / |/| | | |
* | | | | Merge PR #6718: Fix redirection to stderr in lint-repository error message.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6706: ci-common: guess CI_BRANCH for local buildsGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ | |_|_|_|/ / |/| | | | |
| | | | * | Merge anomaly-traces-parser.el into coqdev.el.Gravatar Gaëtan Gilbert2018-02-11
| | | | | |
| | | | * | coqdev.el: add installation instructions.Gravatar Gaëtan Gilbert2018-02-11
| | | | | |
| | * | | | Fix redirection to stderr in lint-repository error message.Gravatar Gaëtan Gilbert2018-02-08
| |/ / / / |/| | | |
| | | | * pre-commit: nicer messagesGravatar Gaëtan Gilbert2018-02-08
| | | | |
| | | | * pre-commit: fail gracefully if fixing whitespace removes all changesGravatar Gaëtan Gilbert2018-02-08
| | | | |
| | | | * pre-commit: add files after fixing ending newlines.Gravatar Gaëtan Gilbert2018-02-08
| | | | |
| | | | * Have the pre-commit hook also fix end-of-file nlGravatar Jason Gross2018-02-08
| | | | |
| | | | * Auto-create .git/hooks/pre-commit on ./configureGravatar Jason Gross2018-02-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | * pre-commit hook: fix whitespace error detectionGravatar Gaëtan Gilbert2018-02-08
| | | | | | | | | | | | | | | | | | | | --quiet implies --exit-code
| | | | * A pre-commit hook to magically fix whitespace issues.Gravatar Gaëtan Gilbert2018-02-08
| | | | |
* | | | | Merge PR #6610: Points to Flocq official repository.Gravatar Maxime Dénès2018-02-07
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6686: Kernel/checker reduction cleanups around projection unfoldingGravatar Maxime Dénès2018-02-07
|\ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 01:02:41 +0000