| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-09-26 | Use default GTK styles for CoqIDE tags. | Pierre-Marie Pédrot | |
| 2015-09-25 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-09-25 | The -require option now accepts a logical path instead of a physical one. | Pierre-Marie Pédrot | |
| 2015-09-25 | Updating the documentation and the toolchain w.r.t. the change in -compile. | Pierre-Marie Pédrot | |
| 2015-09-25 | The -compile option now accepts ".v" files and outputs a warning otherwise. | Pierre-Marie Pédrot | |
| 2015-09-24 | Fixing unsetting of CoqIDE tags. | Pierre-Marie Pédrot | |
| 2015-09-23 | Hopefully better names to constructors of internal_flag, as discussed | Hugo Herbelin | |
| with Enrico. | |||
| 2015-09-23 | Give a way to control if the decidable-equality schemes are built like | Hugo Herbelin | |
| in 8.4 with the schemes of the subcomponent of an inductive added to the environment or discharged as let-ins over the main scheme. As of today, decidable-equality schemes are built when calling vernacular command (Inductive with option Set Dedicable Equality Schemes, or Scheme Equality), so there is no need to discharge the sub-schemes as let-ins. But if ever the schemes are built from within an opaque proof and one would not like the schemes and a fortiori the subschemes to appear in the env, the new addition of a parameter internal_flag to "find_scheme" allows this possibility (then to be set to KernelSilent). | |||
| 2015-09-23 | Removing the generalization of the body of inductive schemes from | Hugo Herbelin | |
| Auto_ind_decl over the internal lemmas. The schemes are built in the main process and the internal lemmas are actually already also in the environment. | |||
| 2015-09-22 | Fixing bug #4207: setoid_rewrite creates self-referring hypotheses. | Pierre-Marie Pédrot | |
| We purge the environment given to the morphism searcher from all dependencies on the considered variable. I hope it is not too costly. | |||
| 2015-09-22 | Fixing fake_ide. | Pierre-Marie Pédrot | |
| 2015-09-21 | Fixing tutorial. | Pierre-Marie Pédrot | |
| The V7 to V8 translator lost part of term annotations. | |||
| 2015-09-21 | Change the default modifiers for navigation. (Fix bug #4295) | Guillaume Melquiond | |
| On most systems (including Windows, according to the bug report), shortcuts Ctrl+Alt+Arrows are preempted by the window manager by default. So don't use them for navigation in Coqide by default. Note that this change only has an impact when installing on a fresh system; it won't change anything for existing users. | |||
| 2015-09-20 | Proof: suggest Admitted->Qed only if the proof is really complete (#4349) | Enrico Tassi | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |