| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-09-20 | Rich printing of CoqIDE protocol failure. | Pierre-Marie Pédrot | |
| 2015-09-20 | Rich printing of messages. | Pierre-Marie Pédrot | |
| 2015-09-20 | Rich printing of goals. | Pierre-Marie Pédrot | |
| 2015-09-20 | Adding rich printing primitives. | Pierre-Marie Pédrot | |
| 2015-09-20 | Do not canonicalize messages received by CoqIDE. | Pierre-Marie Pédrot | |
| 2015-09-20 | Pluging in tag preferences into buffer printing. | Pierre-Marie Pédrot | |
| 2015-09-20 | Adding standard printing tags to CoqIDE. | Pierre-Marie Pédrot | |
| 2015-09-20 | Adding a tag preference | Pierre-Marie Pédrot | |
| 2015-09-20 | Print Assumptions shows engagement. | Maxime Dénès | |
| Seems to be morally required since we have the -type-in-type flag. | |||
| 2015-09-20 | Nametab: print debug notice only in debug mode. | Maxime Dénès | |
| 2015-09-20 | Remove unused type_in_type field in safe_env. | Maxime Dénès | |
| Was left over after Hugo's 9c732a5c878b. | |||
| 2015-09-20 | Test file for #3948 - Anomaly: unknown constant in Print Assumptions. | Maxime Dénès | |
| 2015-09-20 | Revert "On MacOS X, ensuring that files found in the file system have the" | Maxime Dénès | |
| and "Continuing incomplete 4b5af0d6e9ec1 (on MacOS X, ensuring that files" and "Continuing 4b5af0d6e9 and 69941d4e19 about filename case check on MacOS X." This reverts commits 4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606 and 69941d4e195650bf59285b897c14d6287defea0f and e7043eec55085f4101bfb126d8829de6f6086c5a. Trying to emulate a case sensitive file system on top of a case aware one is too costly: 3x slowdown when compiling the stdlib or CompCert. | |||
| 2015-09-20 | Fix #3948 Anomaly: unknown constant in Print Assumptions | Maxime Dénès | |
| Substitution on bound modules was incorrectly extended without sequential composition. | |||
| 2015-09-20 | Better debug printers for module paths. | Maxime Dénès | |
| Now distinguishes between bound modules (Top#X) and submodules (Top.X). Could be useful for the regular printer as well (e.g. in error messages), but I don't know what the compatibility constraints are, so leaving it as it is for now. | |||
| 2015-09-18 | Do not compress match constructs when the inner match contains no branch. ↵ | Guillaume Melquiond | |
| (Fix bug #4348) | |||
| 2015-09-17 | Fix previous merge. | Maxime Dénès | |
| 2015-09-17 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-09-17 | Revert changes in Makefile.build done as part of 2bc88f9a. | Maxime Dénès | |
| If it was intentional, please commit again separately. | |||
| 2015-09-17 | Fix Windows installer. | Guillaume Melquiond | |
| The theories/ directory contains no cmi/cmxs files when native_compute is disabled, so do not try to ship them. | |||
| 2015-09-16 | In pat/constr introduction patterns, fixing in a better way clearing problems | Hugo Herbelin | |
| of temporary hypotheses than 76f27140e6e34 did. | |||
| 2015-09-16 | Explain new flags for native_compute in CHANGES. | Maxime Dénès | |
| 2015-09-16 | Disable native_compute on Windows by default. | Maxime Dénès | |
| Native_compute is not working properly on Windows due to command line size limitations and the lack of namespaces in OCaml. Using compiler-libs could solve this, but it is unclear how to ensure stability w.r.t. future versions of OCaml. | |||
| 2015-09-16 | In configure: -no-native-compiler -> -native-compiler no | Maxime Dénès | |
| 2015-09-16 | Continuing investigation on how to preserve the locality of the action | Hugo Herbelin | |
| of "apply ... in ... as ..." in the context. Fixing a regression done by 7e00e8d60 and f2130a88e1: when an evar is created, the statement of the refined hypothesis virtually depends on the whole context and has to be left at the top. | |||
| 2015-09-16 | Change coq_makefile's default from "-Q . Top" to "-R . Top". (Fix bug #3603) | Guillaume Melquiond | |
| 2015-09-16 | Properly handle {|...|} patterns when patterns are not asymmetric. (Fix bug ↵ | Guillaume Melquiond | |
| #4268) | |||
| 2015-09-15 | Removing a warning in CoqOps. | Pierre-Marie Pédrot | |
| 2015-09-15 | Test for bug #4269. | Pierre-Marie Pédrot | |
| 2015-09-15 | Fixing bug #4269: [Print Assumptions] lies about which axioms a term depends on. | Pierre-Marie Pédrot | |
| This was because the traversal algorithm used canonical names instead of user names, confusing which term was defined and which term was an axiom. | |||
| 2015-09-15 | STM: Reset takes Ltac <ident> into account (Close #4316) | Enrico Tassi | |
| 2015-09-14 | Univs: Add universe binding lists to definitions | Matthieu Sozeau | |
| ... lemmas and inductives to control which universes are bound and where in universe polymorphic definitions. Names stay outside the kernel. | |||
| 2015-09-14 | Remove dead code in lazy reduction machine. | Maxime Dénès | |
| 2015-09-13 | Coq_makefile: read TIMED and TIMECMD from environment. | Maxime Dénès | |
| Useful e.g. with submakefiles. | |||
| 2015-09-13 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-09-12 | Fixing bug #2498: Coqide navigation preferences delayed effect. | Pierre-Marie Pédrot | |
| 2015-09-10 | typo in refman. | Pierre Courtieu | |
| 2015-09-10 | Assertion checking that invariant enforced by 0f8d1b92 always holds. | Maxime Dénès | |
| When reifying a 31-bit integer after a VM computation, we check that no bit outside the 31 LSB is set to 1. | |||
| 2015-09-10 | fresh now accepts more things than just identifiers. | Pierre Courtieu | |
| Namely, it accepts, variables, constants, inductives and constructors. When these have a qualified name, the fresh is done on its basename. | |||
| 2015-09-10 | Fixing previous patch. | Pierre-Marie Pédrot | |
| 2015-09-10 | Fixing the XML lexer definition of names to match the standard. | Pierre-Marie Pédrot | |
| 2015-09-10 | Extending the grammar for CoqIDE preferences so as to match trunk. | Pierre-Marie Pédrot | |
| 2015-09-09 | Merge remote-tracking branch 'origin/v8.5' into trunk | Hugo Herbelin | |
| 2015-09-08 | Emphasizing that eta for vectors is an instance of caseS, as pointed | Hugo Herbelin | |
| out to me by Pierre B. Also extending use of bullets in Vectors where relevant. | |||
| 2015-09-08 | Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commits | Hugo Herbelin | |
| ago) which broke compilation of theories/Logic/WKL.v (collision between a temporary name and a user name). | |||
| 2015-09-08 | Minor modifications to WeakFanTheorem. | Hugo Herbelin | |
| 2015-09-08 | Ensuring that patterns of the form pat/constr move the hypotheses replacing | Hugo Herbelin | |
| an initial hypothesis hyp at the same position in the context. Ensuring the same for "apply c in hyp as pat". Ensuring that "pose proof (H ...) as H" does not change the position of H. | |||
| 2015-09-08 | Short cosmetic changes in tactics.ml. | Hugo Herbelin | |
| 2015-09-08 | A bit of documentation of OCaml code for intro_patterns. | Hugo Herbelin | |
| 2015-09-08 | New option "Unset Bracketing Last Introduction Pattern" for preserving | Hugo Herbelin | |
| compatibility with the non uniform behavior that "intros [] []" on "A*B->C*D->E" automatically introduces A and B but leaves C and D in the goal. Kept unset in 8.5 but planned to be set in 8.6. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |