| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-02-19 | Adding a possible DEPRECATED flag to VERNAC EXTEND statements. | Pierre-Marie Pédrot | |
| 2015-02-19 | Record type for VERNAC EXTEND rules and a bit of documentation. | Pierre-Marie Pédrot | |
| 2015-02-19 | When looking for restrictions in ?n=?p problems, keep the type of let-bindings. | Hugo Herbelin | |
| Bindings of the form [let x:T := M] are unfolded into [(M:T)], so that occur-check is done in [T] as well as in [M] (except when [M] is a variable, where it is hopefully not necessary). This is a way to fix #4062 (evars with type depending on themselves). The fix modifies the alias map (make_alias_map) but it should behave the same at all places using alias maps other than has_constrainable_free_vars. | |||
| 2015-02-18 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-18 | Fix bug #3938 | Matthieu Sozeau | |
| 2015-02-18 | Fix bug #4046. | Matthieu Sozeau | |
| 2015-02-17 | Deprecated options issue a warning. | Pierre-Marie Pédrot | |
| 2015-02-17 | Remove Whelp commands. | Maxime Dénès | |
| Although these commands were never deprecated, they have been unusable for some time now, since they send requests to an Italian server which is no longer alive. | |||
| 2015-02-17 | Separate index for vernacular options. | Maxime Dénès | |
| 2015-02-17 | Remove documentation of non-existing Show Implicits command. | Maxime Dénès | |
| 2015-02-17 | Remove non-existing Tactic Definition command from index. | Maxime Dénès | |
| 2015-02-17 | Fix sentence that was cut in doc of Local Set. | Maxime Dénès | |
| 2015-02-17 | Fixing bug #4053. | Pierre-Marie Pédrot | |
| 2015-02-17 | Fixing bug #4023 again. | Pierre-Marie Pédrot | |
| 2015-02-17 | Tentative fix for bug #2855. | Pierre-Marie Pédrot | |
| 2015-02-17 | CoqIDE: read-only Qed sentence reflected in colors (Close: 4051) | Enrico Tassi | |
| 2015-02-16 | Remove some dead code and add test-suite file. | Matthieu Sozeau | |
| 2015-02-16 | Add test-suite file for #3960. | Matthieu Sozeau | |
| 2015-02-16 | Better comment for [type_of_global_unsafe]. | Matthieu Sozeau | |
| 2015-02-16 | Comment on the unsafe_ functions in Global. | Matthieu Sozeau | |
| 2015-02-16 | Test for bug #3922. | Pierre-Marie Pédrot | |
| 2015-02-16 | STM: when async_proofs_full is set process only tasks in the perspective | Enrico Tassi | |
| This change fixes performance problems in PIDE based user interfaces | |||
| 2015-02-16 | *Queue: API to wake up all threads | Enrico Tassi | |
| 2015-02-16 | Fix bug #3960: potential evar instance categorized as an unresolvable | Matthieu Sozeau | |
| goal in Instance. Also remove some dead code. | |||
| 2015-02-16 | Using same code for browsing physical directories in coqtop and coqdep. | Hugo Herbelin | |
| In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error), - uniformly expecting paths in Unix format and warning otherwise. | |||
| 2015-02-16 | Using home-made ocamllibdep rather than coqdep_boot. | Hugo Herbelin | |
| 2015-02-16 | New short stand-alone ocamllibdep to build .mllib dependencies files. | Hugo Herbelin | |
| 2015-02-16 | Restricting the need for coqdep_boot to mllib.d files (since ocaml | Hugo Herbelin | |
| 3.12.1, ocamldep was able to deal with .ml4, so that building .mllib.d is the only feature that coqdep_boot was still required for). | |||
| 2015-02-16 | Documenting "induction t in ctx" when ctx contains an hyp not mentioning t. | Hugo Herbelin | |
| 2015-02-16 | Fixing bug #4035 (support for dependent destruction within ltac code). | Hugo Herbelin | |
| 2015-02-16 | Test for #2946 (trunk bug with let's in unification). | Hugo Herbelin | |
| 2015-02-16 | Fixing test for bug #3944. | Pierre-Marie Pédrot | |
| 2015-02-16 | Test for bug #3944. | Pierre-Marie Pédrot | |
| 2015-02-16 | Fixing bug #3944. | Pierre-Marie Pédrot | |
| 2015-02-15 | Fixing bug #4037. | Pierre-Marie Pédrot | |
| 2015-02-15 | Changing default for CoqIDE project to append arguments. | Pierre-Marie Pédrot | |
| Implement wish #3582. | |||
| 2015-02-15 | CoqIDE now remembers the path of the last opened project. | Pierre-Marie Pédrot | |
| Fixes bug #2762. | |||
| 2015-02-15 | Selecting whole words on double-click in CoqIDE. | Pierre-Marie Pédrot | |
| Fixes bug #4026. | |||
| 2015-02-15 | Undo: back to 8.4 semantics (Close #3514) | Enrico Tassi | |
| Only tactics are taken into account. | |||
| 2015-02-15 | Reset "section name" works again (Close #3933) | Enrico Tassi | |
| 2015-02-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-15 | Fix test-suite file. Check that definitions do work when sharing is | Matthieu Sozeau | |
| disabled in the kernel. | |||
| 2015-02-15 | Fix 'don't expose cases' in cbn | Pierre Boutillier | |
| 2015-02-15 | Note about "Undo. Undo." in CHANGES | Enrico Tassi | |
| 2015-02-15 | Test for bug #3490. | Pierre-Marie Pédrot | |
| 2015-02-15 | Fixing bug #3490. | Pierre-Marie Pédrot | |
| 2015-02-15 | Test for bug #3916. | Pierre-Marie Pédrot | |
| 2015-02-15 | Fixing bug #3916. | Pierre-Marie Pédrot | |
| 2015-02-15 | Fixing test-suite. | Pierre-Marie Pédrot | |
| 2015-02-15 | Document the behavior change of Instance wrt {|...|}. (Fix for bug #3749) | Guillaume Melquiond | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |