| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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 | 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. | |||
| 2015-09-08 | Fixing clearing of temporary hypotheses with intro pattern pat/constr. | Hugo Herbelin | |
| 2015-09-08 | Fixing "pose proof (H ...) as H" and "assert (H:=H ...) which were supposed | Hugo Herbelin | |
| to behave like "specialize (H ...)" since 4/8/2008 (r11300, 7d515acbc5). | |||
| 2015-09-08 | Hacking parser so as to support both [> ... ] and [id]. | Hugo Herbelin | |
| This (at least technically) solves the issue #4113 (see also #4329). | |||
| 2015-09-08 | Adding a proof of eta on Vector.t of non-zero size. | Hugo Herbelin | |
| 2015-09-08 | Documenting the code when preference is given to expansion of default | Hugo Herbelin | |
| clause in pattern-matching or not. | |||
| 2015-09-08 | Documenting the new behaviour of the Shrink Obligations flag. | Pierre-Marie Pédrot | |
| 2015-09-08 | All Program obligations now respect the Shrink Obligation flag. | Pierre-Marie Pédrot | |
| This allows to reduce the dependencies of subproofs generated by any sequence of tactics. Grants wish #4327. | |||
| 2015-09-08 | More potentialities in proof_terminators. | Pierre-Marie Pédrot | |
| 2015-09-08 | Opacifying the proof_terminator type. | Pierre-Marie Pédrot | |
| 2015-09-08 | Fixing the Shrink Obligations option. | Pierre-Marie Pédrot | |
| Let-bindings were not taken into account, resulting in proof-terms way too huge. | |||
| 2015-09-06 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-09-06 | Output a warning when conversion compilation failed. | Maxime Dénès | |
| Previously, the kernel would silently fall back to standard conversion. | |||
| 2015-09-06 | Fix a bug in 31 bit arithmetic, leading to failing conversion tests. | Maxime Dénès | |
| On 64 bits architectures, integers could have some of their 32 msb set to 1 internally in the VM. When read back to a Coq term, this was not observable. But an equality test would fail. From the user point of view, the symptom was that vm_compute; reflexivity would succeed but the subsequent Qed would fail. Bug reported by Tahina Ramananandro. | |||
| 2015-09-06 | Fixed critical bug in 31 bit arithmetic of VM | Catalin Hritcu | |
| ADDMULDIVINT31 was missing pops in some cases | |||
| 2015-09-06 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-09-06 | Adding a Makefile target for the MSets and MMaps directories. | Pierre-Marie Pédrot | |
| The target creation process should eventually be automated, because it is tedious and error-prone as witnessed by this commit. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |