| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-08 | Axioms now support the universe binding syntax. | Pierre-Marie Pédrot | |
| We artificially restrict the syntax though, because it is unclear of what the semantics of several axioms in a row is, in particular about the resolution of remaining evars. | |||
| 2015-10-08 | f_equal fix continued: do a refresh_universes as before. | Matthieu Sozeau | |
| 2015-10-08 | aux_file: export API to ease writing of a Proof Using annotator. | Enrico Tassi | |
| 2015-10-08 | Proof using: let-in policy, optional auto-clear, forward closure* | Enrico Tassi | |
| - "Proof using p*" means: use p and any section var about p. - Simplify the grammar/parser for proof using <expression>. - Section variables with a body (let-in) are pulled in automatically since they are safe to be used (add no extra quantification) - automatic clear of "unused" section variables made optional: Set Proof Using Clear Unused. since clearing section hypotheses does not "always work" (e.g. hint databases are not really cleaned) - term_typing: trigger a "suggest proof using" message also for Let theorems. | |||
| 2015-10-08 | term_typing: strengthen discharging code | Enrico Tassi | |
| Given the way Lib.extract_hyps is coded if the const_hyps field of a constant declaration contains a named_context that does not have the same order of the one in Environment.env, discharging is broken (as in some section variables are not discharged). If const_hyps is computed by the kernel, then the order is correct by construction. If such list is provided by the user, the order is not granted. We now systematically sort the list of user provided section hyps. The code of Proof using is building the named_context in the right order, but the API was not enforcing/checking it. Now it does. | |||
| 2015-10-08 | CThread: blocking read + threads now works | Enrico Tassi | |
| 2015-10-08 | Spawn: use each socket exclusively for writing or reading | Enrico Tassi | |
| According to http://caml.inria.fr/mantis/view.php?id=5325 you can't use the same socket for both writing and reading. The result is lockups (may be fixed in 4.03). | |||
| 2015-10-08 | STM: for PIDE based UIs, edit_at requires no Reach.known_state | Enrico Tassi | |
| 2015-10-08 | Future: make not-here/not-ready messages customizable | Enrico Tassi | |
| 2015-10-08 | STM: fix backtrace handling | Enrico Tassi | |
| 2015-10-08 | Goptions: new value type: optional string | Enrico Tassi | |
| These options can be set to a string value, but also unset. Internal data is of type string option. | |||
| 2015-10-07 | Remove the "exists" overrides from Program. (Fix bug #4360) | Guillaume Melquiond | |
| 2015-10-07 | Fix bug #4069: f_equal regression. | Matthieu Sozeau | |
| 2015-10-07 | Univs: fix FingerTree contrib. | Matthieu Sozeau | |
| Let merge_context_set be lenient when merging the context of side effects of an entry from solve_by_tac. | |||
| 2015-10-07 | Test for record syntax parsing. | Pierre-Marie Pédrot | |
| 2015-10-07 | Record fields accept an optional final semicolon separator. | Pierre-Marie Pédrot | |
| There is no such thing as the OPTSEP macro in Camlp4 so I had to expand it by hand. | |||
| 2015-10-07 | Univs: add Strict Universe Declaration option (on by default) | Matthieu Sozeau | |
| This option disallows "declare at first use" semantics for universe variables (in @{}), forcing the declaration of _all_ universes appearing in a definition when introducing it with syntax Definition/Inductive foo@{i j k} .. The bound universes at the end of a definition/inductive must be exactly those ones, no extras allowed currently. Test-suite files using the old semantics just disable the option. | |||
| 2015-10-06 | Fixing emacs output in debugging mode. | Pierre Courtieu | |
| Goal displaying during Debugging ltac is a notice message now. Other messages are debug messages. This does not change anything in coqide or coqtop, but allows proofgeneral to dispatch them in the right buffers (pg had to be fixed too). | |||
| 2015-10-06 | Univs (pretyping): call vm_compute/native_compute with the current | Matthieu Sozeau | |
| universe graph | |||
| 2015-10-06 | Fix bug #4354: interpret hints in the right env and sigma. | Matthieu Sozeau | |
| 2015-10-05 | Univs: fix bug #4288, Print Sorted generated backward < constraints. | Matthieu Sozeau | |
| 2015-10-05 | Univs: fix printing bug #3797. | Matthieu Sozeau | |
| 2015-10-05 | Update the .mailmap file. | Guillaume Melquiond | |
| The update process is as follows: run "git shortlog -s -e" and look for duplicate or missing contributors. | |||
| 2015-10-05 | Univs: fix handling of evar_map in identity coercion construction. | Matthieu Sozeau | |
| 2015-10-04 | Fix typo. (Fix bug #4355) | Guillaume Melquiond | |
| 2015-10-02 | Mark the Coq.Compat files for documentation. (Fix bug #4353) | Guillaume Melquiond | |
| 2015-10-02 | Updating versions history with data from Gérard. | Hugo Herbelin | |
| Adding Gérard's history file about V1-V5 versions. | |||
| 2015-10-02 | Fixing error messages about Hint. | Hugo Herbelin | |
| 2015-10-02 | Improving reference manual in that auto uses simple apply rather than apply. | Hugo Herbelin | |
| Still, there are small differences, e.g. on "use_metas_eagerly_in_conv_on_closed_terms", but also maybe in some amount of use of delta that Matthieu would know better than me if it matters or not in practice. | |||
| 2015-10-02 | Update the history of versions with recent versions. | Hugo Herbelin | |
| 2015-10-02 | Univs: Change intf of push_named_def to return the computed universe | Matthieu Sozeau | |
| context Let-bound definitions can be opaque but the whole universe context was not gathered to be discharged at section closing time. | |||
| 2015-10-02 | Univs: refined handling of assumptions | Matthieu Sozeau | |
| According to their polymorphic/non-polymorphic status, which imply that universe variables introduced with it are assumed to be >= or > Set respectively in the following definitions. | |||
| 2015-10-02 | Univs: fix checker generating undeclared universes. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix test-suite file for #4287, now properly rejected. | Matthieu Sozeau | |
| 2015-10-02 | Univs: Remove test-suite file #3309 | Matthieu Sozeau | |
| This relied on universes lower than Prop. A proper test for the sharing option should be found, -type-in-type is not enough either. | |||
| 2015-10-02 | Univs: fix test-suite file (4301 is invalid, but a good regression test) | Matthieu Sozeau | |
| 2015-10-02 | Fix after rebase... | Matthieu Sozeau | |
| 2015-10-02 | Univs: forgot a substitution in mod_typing. | Matthieu Sozeau | |
| 2015-10-02 | Univs: correct handling of with in modules | Matthieu Sozeau | |
| For polymorphic and non-polymorphic parameters and definitions, fixes bugs #4298, #4294 | |||
| 2015-10-02 | Univs: the stdlib now needs 5 universes | Matthieu Sozeau | |
| Prop < Set < i for every global univ i | |||
| 2015-10-02 | Univs: fix bug #4251, handling of template polymorphic constants. | Matthieu Sozeau | |
| 2015-10-02 | Univs: update checker | Matthieu Sozeau | |
| 2015-10-02 | Univs: fixed 3685 by side-effect :) | Matthieu Sozeau | |
| 2015-10-02 | Univs: minor fixes to test-suite files | Matthieu Sozeau | |
| 108 used an implicit lowering to Prop. | |||
| 2015-10-02 | Univs: fix handling of evd's universes and side effects in build_by_tactic | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix semantics of Type in proof mode in universe-polymorphic mode | Matthieu Sozeau | |
| Allowing universes to be instantiated if the body of the proof requires it (the levels stay flexible). Not allowed for non-polymorphic cases, to be compatible with the stm's invariant that the type should not change. | |||
| 2015-10-02 | Univs: fix minimization to allow lowering a universe to Set, not Prop. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix inference of the lowest sort for records. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix subtyping of polymorphic parameters. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix evar_map handling in Hint processing. | Matthieu Sozeau | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |