| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-02-20 | Add CHANGES entry for decimals in prelude | Jason Gross | |
| 2018-02-20 | Update SearchPattern.out for numeral notations | Jason Gross | |
| There is more churn than there should be because SearchPattern uses a non-local sorting algorithm; the comparison function considers many constants equal in priority and leaves it up to the heap structure to break ties, which seems wrong. This has been reported as [bug #5573](https://coq.inria.fr/bugs/show_bug.cgi?id=5573). | |||
| 2018-02-20 | Doc: add Decimal-related files to index-list.html.template | Jason Gross | |
| 2018-02-20 | Decimal goodies : conversion to/from Coq strings | Pierre Letouzey | |
| Just because it's fun and easy. Not used by the Numeral Notation command. | |||
| 2018-02-20 | Decimal: proofs that conversions from/to nat,N,Z are bijections | Pierre Letouzey | |
| 2018-02-20 | Decimal: simple representation of base-10 numbers | Pierre Letouzey | |
| 2018-02-19 | Merge PR #6728: Extrude monomorphic universe contexts from with Definition ↵ | Maxime Dénès | |
| constraints. | |||
| 2018-02-19 | Merge PR #6761: Remove unused argument in Record.declare_structure | Maxime Dénès | |
| 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 #6230: Better Cemitcodes API + compact relocation representation | Maxime Dénès | |
| 2018-02-19 | Merge PR #6759: detype_case predicate is not optional | Maxime Dénès | |
| 2018-02-19 | Merge PR #6772: Cleanup inferCumulativity | Maxime Dénès | |
| 2018-02-19 | Merge PR #6648: [tactics] make apply_type safe | 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-19 | Merge PR #6478: [build] Fix VM dynamic linking prep in byte builds. | Maxime Dénès | |
| 2018-02-19 | Merge PR #6571: Fix ci-all target | 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-16 | apply_type: add option "typecheck" passed down to refine | Enrico Tassi | |
| 2018-02-16 | Cleaner treatment of parameters in inferCumulativity | Gaëtan Gilbert | |
| No using a mutable counter to skip them, instead we keep them in the environment. | |||
| 2018-02-16 | Fix reduction flags in inferCumulativity | Gaëtan Gilbert | |
| The only difference is when we have a rel local definition in the initial environment, which isn't actually possible. However that depends on the specific way we treat parameters. | |||
| 2018-02-16 | Adding a test for the construction that was broken in Coccinelle. | Pierre-Marie Pédrot | |
| There was no test in the test-suite checking for double with-def constraints in module typing. | |||
| 2018-02-16 | Extrude monomorphic universe contexts from with Definition constraints. | Pierre-Marie Pédrot | |
| We defer the computation of the universe quantification to the upper layer, outside of the kernel. | |||
| 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-15 | [ide] Localize a IDE-specific flag. | Emilio Jesus Gallego Arias | |
| 2018-02-15 | Merge PR #1073: new quick2vo target: like vio2vo, but smarter | Maxime Dénès | |
| 2018-02-15 | disable tests: vio2vo is broken in Windows | Ralf Jung | |
| 2018-02-15 | also test vio2vo | Ralf Jung | |
| 2018-02-15 | test "make quick2vo" | Ralf Jung | |
| 2018-02-15 | new quick2vo target: like vio2vo, but smarter | Ralf Jung | |
| 2018-02-15 | Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProject | Maxime Dénès | |
| 2018-02-15 | coq_makefile: Support "" as the prefix in _CoqProject | Joachim Breitner | |
| This fixes #6350 (and even comes with a test case). Refering to other directories as `-R … ""` is maybe not best practice, but some people out there do it, so as long as it does not cause too much trouble, we can continue to support it. | |||
| 2018-02-15 | Merge PR #6760: CHANGES for 8.7.2. | Maxime Dénès | |
| 2018-02-14 | CHANGES for 8.7.2. | Théo Zimmermann | |
| 2018-02-14 | Remove unused argument in Record.declare_structure | Gaëtan Gilbert | |
| This was for autoinstance. | |||
| 2018-02-14 | Factorize the relocations in the on-disk VM representation. | Pierre-Marie Pédrot | |
| Instead of using a linear representation, we simply use a table that maps every kind of relocation to the list of positions it needs to be applied to. | |||
| 2018-02-14 | Use a more compact representation for bytecode relocations stored on disk. | Pierre-Marie Pédrot | |
| The previous implementation used a list of pairs, which has size 9n where n is the number of relocations. We instead use two arrays for a total memory cost of 2n + 5 words. The use of arrays may turn out to be problematic on 32-bit machines, I am unsure if we will hit this limitation in practice. | |||
| 2018-02-14 | Do not use global variables for VM bytecode compilation in Cemitcodes. | Pierre-Marie Pédrot | |
| Instead we thread a buffer. | |||
| 2018-02-14 | Remove the unsafe bytes conversion function in Cemitcodes. | Pierre-Marie Pédrot | |
| This is actually not needed, as the only thing we do with this Bytes.t is to pass it to a C function which will use it in a read-only way. | |||
| 2018-02-14 | Move the call to the computation of bytecode inside Cemitcodes. | Pierre-Marie Pédrot | |
| This shouldn't matter because the tcode_of_code function is pure, its only effect being allocating a string and filling it with the translated bytecode. | |||
| 2018-02-14 | Abstract further the type of VM bytecode compilation. | Pierre-Marie Pédrot | |
| This reduces the possibility to wreak havoc while making the API nicer. | |||
| 2018-02-14 | detype_case predicate is not optional | Gaëtan Gilbert | |
| 2018-02-14 | Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation) | Maxime Dénès | |
| 2018-02-14 | Merge PR #6713: Fix #6677: Critical bug with VM and universes | Maxime Dénès | |
| 2018-02-14 | [build] Fix VM dynamic linking prep in byte builds. | Emilio Jesus Gallego Arias | |
| We correctly set the path of `libcoqrun` in non-local builds. This bug was introduced by #6038. c.f. #6475 , #5992. | |||
| 2018-02-13 | coqdev.el: wait for 'compile to touch compilation-error-regexp-alist | Gaëtan Gilbert | |
| (and alist-alist) | |||
| 2018-02-13 | Add CHANGES entry for #1047 | Tej Chajed | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |