| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-04-10 | Adding a test for 'rewrite in *' when an evar is solved by side-effect. | Pierre-Marie Pédrot | |
| 2017-04-10 | Adding a test for the correctness of normalization in legacy typeclasses. | Pierre-Marie Pédrot | |
| This is a test for commit 9d1230d484a2cf519f9cd76dc0f37815f3c6339b. | |||
| 2017-04-10 | Documenting the changes introduced by the EConstr branch. | Pierre-Marie Pédrot | |
| 2017-04-08 | Fix a heuristic used by legacy typeclass resolution. | Pierre-Marie Pédrot | |
| The evarmap used by the heuristic could contain resolved evars, which could lead to a failure of backtracking in the EConstr branch. This is experimental and may be to costly. | |||
| 2017-04-07 | Fix an unhandled exception in Omega. | Pierre-Marie Pédrot | |
| 2017-04-07 | Merge branch 'master' into econstr | Pierre-Marie Pédrot | |
| 2017-04-07 | Remove a forgotten rule for decl_mode from the Makefile. | Pierre-Marie Pédrot | |
| This was making the miniopt target fail. | |||
| 2017-04-07 | Merge PR#530: [toplevel] Remove exception error printer in favor of feedback ↵ | Maxime Dénès | |
| printer. | |||
| 2017-04-07 | Merge PR#519: Faster side effects | Maxime Dénès | |
| 2017-04-07 | Inline the only use of hcons_j in Term_typing. | Pierre-Marie Pédrot | |
| 2017-04-06 | Merge PR#455: Farewell decl_mode | Maxime Dénès | |
| 2017-04-06 | Merge PR#488: Adding a documentation for the new proof engine. | Maxime Dénès | |
| 2017-04-06 | Adding a documentation for the new proof engine. | Pierre-Marie Pédrot | |
| 2017-04-06 | Documenting the fact terms are only hashconsed outside of a section. | Pierre-Marie Pédrot | |
| 2017-04-06 | Merge PR#508: Optimize pending evars | Maxime Dénès | |
| 2017-04-06 | Fix a normalization hotspot in computation of constr keys. | Pierre-Marie Pédrot | |
| Getting a key only needs to observe the root of a term. This hotspot was observed in HoTT. | |||
| 2017-04-06 | Merge PR#542: [travis] Add webhook to Gitter. | Maxime Dénès | |
| 2017-04-06 | [travis] Add webhook to Gitter. | Théo Zimmermann | |
| 2017-04-05 | [toplevel] Remove exception error printer in favor of feedback printer. | Emilio Jesus Gallego Arias | |
| We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing all the errors from the feedback handler, even in the case of coqtop. All error display is handled by a single, uniform path. There may be some minor discrepancies with 8.6 as we are uniform now whereas 8.6 tended to print errors in several ways, but our behavior is a subset of the 8.6 behavior. We had to make a choice for `-emacs` error output, which used to vary too. We have chosen to display error messages as: ``` (location info) option \n (program caret) option \n MARKER[254]Error: msgMARKER[255] ``` This commit also fixes: - https://coq.inria.fr/bugs/show_bug.cgi?id=5418 - https://coq.inria.fr/bugs/show_bug.cgi?id=5429 | |||
| 2017-04-05 | Removing a normalization hotspot from EConstr. | Pierre-Marie Pédrot | |
| It was not necessary to normalize a term just to check whether it was a global reference. The hotspot appeared in mathcomp. | |||
| 2017-04-05 | Merge PR#434: Optimizing array mapping in the kernel. | Maxime Dénès | |
| 2017-04-04 | Merge PR#502: [pp] Add anomaly header to error messages. | Maxime Dénès | |
| 2017-04-04 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 2017-04-03 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-04-03 | Merge PR#533: Instances should obey universe binders even when defined by ↵ | Maxime Dénès | |
| tactics. | |||
| 2017-04-03 | Fix loading of ocamldebug printers. | Pierre-Marie Pédrot | |
| 2017-04-03 | Instances should obey universe binders even when defined by tactics. | Gaetan Gilbert | |
| 2017-04-03 | Merge PR#417: No cast surgery in let in | Maxime Dénès | |
| 2017-04-03 | Add test file for #4957. | Maxime Dénès | |
| Bug #4957 was "unify cannot directly unify universes with evars, but can do so indirectly". | |||
| 2017-04-02 | Fix higher-order pattern variables not being printed as "@?" (bug #5431). | Guillaume Melquiond | |
| 2017-04-02 | Fix documentation typo (bug #5433). | Guillaume Melquiond | |
| 2017-04-02 | Simplify some proofs. | Guillaume Melquiond | |
| This commit does not modify the signature of the involved modules, only the opaque proof terms. One has to wonder how proofs can bitrot so much that several occurrences of "replace 4 with 4" start appearing. | |||
| 2017-04-01 | Restore a fast path in EConstr instance normalization. | Pierre-Marie Pédrot | |
| 2017-04-01 | Using delayed universe instances in EConstr. | Pierre-Marie Pédrot | |
| The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step. | |||
| 2017-04-01 | Declaring ltac plugin, so that static linking works. | Hugo Herbelin | |
| 2017-04-01 | Actually exporting delayed universes in the EConstr implementation. | Pierre-Marie Pédrot | |
| For now we only normalize sorts, and we leave instances for the next commit. | |||
| 2017-03-31 | Make the Constr.kind_of_term type parametric in sorts and universes. | Pierre-Marie Pédrot | |
| 2017-03-31 | Ensuring proper cast invariants in EConstr.kind. | Pierre-Marie Pédrot | |
| The kernel does fishy things with casts, such that ensuring there are no two consecutive VMcast or NATIVEcast in terms. We enforce this in EConstr view as well. | |||
| 2017-03-31 | Revert "Specially crafted EConstr.kind to be more efficient." | Pierre-Marie Pédrot | |
| This reverts commit b5f07be9fdcd41fdaf73503e5214e766bf6a303b. The performance difference was not conclusive enough to pay for the code ugliness. | |||
| 2017-03-30 | Specially crafted EConstr.kind to be more efficient. | Pierre-Marie Pédrot | |
| We do one step of loop unrolling, limit the number of allocations and mark the function as inline. | |||
| 2017-03-30 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-03-30 | Merge PR#463: Run non-tactic comands without resilient_command | Maxime Dénès | |
| 2017-03-30 | Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R. | Guillaume Melquiond | |
| 2017-03-30 | Merge PR#469: Added take to VectorDef | Maxime Dénès | |
| 2017-03-30 | Added take to VectorDef. | George Stelle | |
| Added a function that takes the first [p] elements of a vector, and a few lemmas proving some of its properties. | |||
| 2017-03-30 | Merge PR#511: [stm] Remove some obsolete vernacs/classification. | Maxime Dénès | |
| 2017-03-29 | Merge PR#522: [coqide] Protect against size_allocate race in proofview. | Maxime Dénès | |
| 2017-03-29 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-03-29 | Merge PR#514: [travis] Backport from trunk: VST | Maxime Dénès | |
| 2017-03-29 | Merge PR#506: [nit] Fix a couple incorrect uses of msg_error. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |