| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-06-13 | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) | Pierre Letouzey | |
| 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. | |||
| 2017-06-12 | Merge PR#709: Bytecode compilation apart from 'make world', again | Maxime Dénès | |
| 2017-06-01 | 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-05-31 | Tests for new specialize feature + CHANGES. | Pierre Courtieu | |
| 2017-05-30 | Documentation for eassert, eenough, epose proof, eset, eremember, epose. | Hugo Herbelin | |
| Includes fixes and suggestions from Théo. | |||
| 2017-05-25 | 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-23 | enters coq_makefile2 | Enrico Tassi | |
| 2017-05-23 | [vernac] Remove `Save thm id.` command. | Emilio Jesus Gallego Arias | |
| 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... | |||
| 2017-05-22 | Clarifying the interpretation path for the "constr_with_binding" argument. | Hugo Herbelin | |
| 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. | |||
| 2017-05-17 | Merge PR#457: Adding an even more compact goal hyps mode. | Maxime Dénès | |
| 2017-05-13 | Aligning on standard layout of CHANGES. | Hugo Herbelin | |
| 2017-05-11 | Documenting Printing Compact Contexts + CHANGES | Pierre Courtieu | |
| 2017-04-27 | Tentative note in CHANGES about now applying βι while typing "match" branches. | Hugo Herbelin | |
| 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. | |||
| 2017-04-19 | CHANGES entry for #545. | Maxime Dénès | |
| 2017-04-11 | Merge PR#379: Introducing evar-insensitive constrs | Maxime Dénès | |
| 2017-04-10 | Documenting the changes introduced by the EConstr branch. | Pierre-Marie Pédrot | |
| 2017-04-07 | [camlpX] Enrico's changes to camlp4 removal. | Emilio Jesus Gallego Arias | |
| This removes some remaining support for camlp4 in the infrastructure and documents the change. | |||
| 2017-04-06 | Merge PR#455: Farewell decl_mode | Maxime Dénès | |
| 2017-03-22 | Document the changes to IZR. | Guillaume Melquiond | |
| 2017-03-07 | Farewell decl_mode | Enrico Tassi | |
| This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests. | |||
| 2017-03-03 | CHANGES: choice over setoids and prop. ext. | Hugo Herbelin | |
| 2017-01-19 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-12-07 | A few words in CHANGES. | Maxime Dénès | |
| 2016-11-30 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-11-24 | Fix some documentation typos. | Guillaume Melquiond | |
| Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else. | |||
| 2016-11-18 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-11-16 | [doc] Mention XML protocol on changes. | Emilio Jesus Gallego Arias | |
| It may be worth it, also added a note about file reorganization. | |||
| 2016-11-14 | Remove the list of bug fixes from CHANGES. | Maxime Dénès | |
| We could not produce an exhaustive list of such fixes, and the usefulness of such a list is not clear. | |||
| 2016-11-10 | Update CHANGES and credits for 8.6beta1. | Maxime Dénès | |
| 2016-11-07 | Mention notypeclasses refine in CHANGES | Matthieu Sozeau | |
| 2016-11-07 | CHANGES for this branch. | Matthieu Sozeau | |
| 2016-10-29 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-10-26 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-10-25 | Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)." | Maxime Dénès | |
| This reverts commit c9c54122d1d9493a965b483939e119d52121d5a6. This behavior of refine has changed three times in recent years, so let's take the time to make up our mind and wait for a major release. Btw, onhyps=None is not a sane way to express that a tactic should be applied to all hypotheses. | |||
| 2016-10-25 | Update CHANGES. | Maxime Dénès | |
| 2016-10-12 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-10-12 | Allocating a section in CHANGES for changes specific to 8.7. | Hugo Herbelin | |
| 2016-10-12 | Tentatively preparing to add changes specific to v8.7 (see PR #275). | Hugo Herbelin | |
| 2016-10-08 | Report about changes of semantics of auto as an ltac argument (see #4966). | Hugo Herbelin | |
| 2016-10-06 | Remove the Set Verbose Compat option and turn the warning on by default. | Maxime Dénès | |
| These warnings can now be configured like any other, so we don't need a specific option anymore. | |||
| 2016-10-03 | Document change related to Keep Proof Equalities in CHANGES. | Maxime Dénès | |
| 2016-09-29 | Being more informative about the change of behavior of "subst". | Hugo Herbelin | |
| 2016-09-21 | Fix description of change in intro semantics. | Maxime Dénès | |
| 2016-09-15 | Extending "contradiction" so that it recognizes statements such as "~x=x" or ↵ | Hugo Herbelin | |
| ~True. Found 1 incompatibility in tested contribs and 3 times the same pattern of incompatibility in the standard library. In all cases, it is an improvement in the form of the script. New behavior deactivated when version is <= 8.5. | |||
| 2016-09-12 | Refolding: disable in 8.4 compat file, document | Matthieu Sozeau | |
| 2016-08-21 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-08-17 | Fixing CHANGES. | Hugo Herbelin | |
| Option Standard Proposition Elimination Scheme from 8.5 was not documented in the right section. | |||
| 2016-08-17 | Documenting fix of #3070 (subst and chain of dependencies). | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |