| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Correct the option for cumulativity in CHANGES |  Amin Timany | 2017-08-18 |
| | | |||
| * | Use the wording suggested by Gaetan. |  Théo Zimmermann | 2017-08-17 |
| | | |||
| * | Addition suggested by Pierre-Marie. | Théo Zimmermann | 2017-08-17 |
| | | |||
| * | Additions following Hugo's suggestions. | Théo Zimmermann | 2017-08-16 |
| | | |||
| * | Improve wording. | Théo Zimmermann | 2017-08-16 |
| | | |||
| * | 8.7 CHANGES | Théo Zimmermann | 2017-08-16 |
| | | |||
| * | Porting #856 (8.6.1 CHANGES entries) to master | Théo Zimmermann | 2017-08-16 |
| | | |||
| * | Merge PR #925: Document Extraction TestCompile |  Maxime Dénès | 2017-08-01 |
| |\ | |||
| | * | Extraction TestCompile documented + mentionned in CHANGES |  Pierre Letouzey | 2017-07-27 |
| | | | | | | | | | Also includes a minor fix of the Extraction doc (a Require was missing). | ||
| * | | Adding support for recursive notations of the form "x , .. , y , z". |  Hugo Herbelin | 2017-07-26 |
| |/ | | | | | | | | | Since camlp5 parses from left, the last ", z" was parsed as part of an arbitrary long list of "x1 , .. , xn" and a syntax error was raised since an extra ", z" was still expected. We support this by translating "x , .. , y , z" into "x , y , .. , z" and reassembling the arguments appropriately after parsing. | ||
| * | Add an entry to CHANGES about timing in coq_makefile |  Jason Gross | 2017-07-11 |
| | | |||
| * | Update CHANGES with inversion_sigma entry | Jason Gross | 2017-06-30 |
| | | |||
| * | Merge PR#774: [ide] Add route_id parameter to query call. | Maxime Dénès | 2017-06-20 |
| |\ | |||
| | * | [ide] Add route_id parameter to query call. |  Emilio Jesus Gallego Arias | 2017-06-18 |
| | | | | | | | | | | | | | | | | | This is necessary in order for clients to identify the results of queries. This is a minor breaking change of the protocol, affecting only this particular call. This change is necessary in order to fix bug ####. | ||
| * | | Document cumulativity for inductive types | Amin Timany | 2017-06-16 |
| |/ | |||
| * | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) | Pierre Letouzey | 2017-06-13 |
| | | | | | | | See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude. | ||
| * | Merge PR#709: Bytecode compilation apart from 'make world', again | Maxime Dénès | 2017-06-12 |
| |\ | |||
| | * | mention 'make world' without 'byte' in CHANGES + 2 minor suggestions | Pierre Letouzey | 2017-06-01 |
| | | | |||
| * | | Merge PR#449: make specialize smarter (bug 5370). | Maxime Dénès | 2017-06-01 |
| |\ \ | |||
| | * | | Tests for new specialize feature + CHANGES. |  Pierre Courtieu | 2017-05-31 |
| | |/ | |||
| * / | Documentation for eassert, eenough, epose proof, eset, eremember, epose. | Hugo Herbelin | 2017-05-30 |
| |/ | | | | Includes fixes and suggestions from Théo. | ||
| * | Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings | Maxime Dénès | 2017-05-25 |
| |\ | |||
| * \ | Merge PR#406: coq makefile2 | Maxime Dénès | 2017-05-25 |
| |\ \ | |||
| | * | | enters coq_makefile2 |  Enrico Tassi | 2017-05-23 |
| | | | | |||
| * | | | [vernac] Remove `Save thm id.` command. | Emilio Jesus Gallego Arias | 2017-05-23 |
| |/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We'd like to cleanup the `proof_end` type so we can have a smaller path in proof save. Note that the construction: ``` Goal Type. ⋮ Save id. ``` has to be handled by the STM in the same path as Defined (but with an opaque flag), as `Save id` will alter the environment and cannot be processed in parallel. We thus try to simply such paths a bit, as complexity of `lemmas.ml` seems like an issue these days. The form `Save Theorem id` doesn't really seem used, and moreover we should really add a type of "Goal", and unify syntax. It is often the case that beginners try `Goal addnC n : n + 0 = n." etc... | ||
| | * | Clarifying the interpretation path for the "constr_with_binding" argument. | Hugo Herbelin | 2017-05-22 |
| |/ | | | | | | | | | | | | | | | | | This fixes an inconsistency introduced in 554a6c806 (svn r12603) where both interp_constr_with_bindings and interp_open_constr_with_bindings were going through interp_open_constr (no type classes so as to not to commit too early on irreversible choices, accepting unresolved holes). We fix this by having interp_constr_with_bindings going to interp_constr (using type classes and failing on unresolved evars). The external impact is that any TACTIC EXTEND which refers to constr_with_binding has now to decide whether it intends it to use what the name suggest (using type classes and to fail if evars remain unresolved), thus keeping constr_with_binding, or the actual behavior which requires to use open_constr_with_bindings for strict compatibility. | ||
| * | Merge PR#457: Adding an even more compact goal hyps mode. | Maxime Dénès | 2017-05-17 |
| |\ | |||
| * | | Aligning on standard layout of CHANGES. | Hugo Herbelin | 2017-05-13 |
| | | | |||
| | * | Documenting Printing Compact Contexts + CHANGES | Pierre Courtieu | 2017-05-11 |
| | | | |||
| * | | Tentative note in CHANGES about now applying βι while typing "match" branches. | Hugo Herbelin | 2017-04-27 |
| |/ | | | | | | | In practice, this is almost invisible except when using "refine". So, in some sense, it is aligning the behavior of pretyping on the one of logic.ml's "refine" so that the more natural behavior of 8.4's refine on this issue is restored. | ||
| * | CHANGES entry for #545. | Maxime Dénès | 2017-04-19 |
| | | |||
| * | Merge PR#379: Introducing evar-insensitive constrs | Maxime Dénès | 2017-04-11 |
| |\ | |||
| | * | Documenting the changes introduced by the EConstr branch. |  Pierre-Marie Pédrot | 2017-04-10 |
| | | | |||
| * | | [camlpX] Enrico's changes to camlp4 removal. | Emilio Jesus Gallego Arias | 2017-04-07 |
| |/ | | | | | This removes some remaining support for camlp4 in the infrastructure and documents the change. | ||
| * | Merge PR#455: Farewell decl_mode | Maxime Dénès | 2017-04-06 |
| |\ | |||
| * | | Document the changes to IZR. |  Guillaume Melquiond | 2017-03-22 |
| | | | |||
| | * | Farewell decl_mode | Enrico Tassi | 2017-03-07 |
| | | | | | | | | | | | This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests. | ||
| * | | CHANGES: choice over setoids and prop. ext. | Hugo Herbelin | 2017-03-03 |
| |/ | |||
| * | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-01-19 |
| |\ | |||
| | * | A few words in CHANGES. | Maxime Dénès | 2016-12-07 |
| | | | |||
| * | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-11-30 |
| |\| | |||
| | * | Fix some documentation typos. | Guillaume Melquiond | 2016-11-24 |
| | | | | | | | | | | | Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else. | ||
| * | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-11-18 |
| |\| | |||
| | * | [doc] Mention XML protocol on changes. | Emilio Jesus Gallego Arias | 2016-11-16 |
| | | | | | | | | | It may be worth it, also added a note about file reorganization. | ||
| | * | Remove the list of bug fixes from CHANGES. | Maxime Dénès | 2016-11-14 |
| | | | | | | | | | | | We could not produce an exhaustive list of such fixes, and the usefulness of such a list is not clear. | ||
| | * | Update CHANGES and credits for 8.6beta1. | Maxime Dénès | 2016-11-10 |
| | | | |||
| | * | Mention notypeclasses refine in CHANGES |  Matthieu Sozeau | 2016-11-07 |
| | | | |||
| | * | CHANGES for this branch. | Matthieu Sozeau | 2016-11-07 |
| | | | |||
| * | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-29 |
| |\| | |||
| | * | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-26 |
| | |\ | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |