| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-11 | Constr_matching: renaming misleading name stk into ctx. | Hugo Herbelin | |
| 2015-10-10 | Fix a few latex errors in documentation of Proof Using (e.g. \tt*). | Guillaume Melquiond | |
| 2015-10-09 | Complete handling of primitive projections in VM. | Maxime Dénès | |
| This commit is a follow-up to a51cce369b9c634a93120092d4c7685a242d55b1 | |||
| 2015-10-09 | Code cleaning in VM (with Benjamin). | Maxime Dénès | |
| Rename some functions, remove dead code related to (previously deprecated, now removed) option Set Boxed Values. | |||
| 2015-10-09 | Minor typo in universe polymorphism doc. | Maxime Dénès | |
| 2015-10-09 | Refine fix for handling of the universe contexts of hints, depending on | Matthieu Sozeau | |
| their polymorphic status _and_ locality. | |||
| 2015-10-09 | Fix CFGV contrib: handling of global hints introducing global universes. | Matthieu Sozeau | |
| It was wrong, the context was readded needlessly to the local evar_map context. | |||
| 2015-10-09 | Fix Next Obligation to not raise an anomaly in case of mutual | Matthieu Sozeau | |
| definitions. | |||
| 2015-10-09 | Fix inference of return clause raising a type error. | Matthieu Sozeau | |
| 2015-10-09 | STM: Work around an occasional crash in dot (debug output) | Alec Faithfull | |
| The splines=ortho option seems to make dot crash sometimes, so this commit removes it from the STM debugging output | |||
| 2015-10-09 | TQueue: Allow some tasks to be saved when clearing a TQueue | Alec Faithfull | |
| 2015-10-09 | TQueue: Expose the length of TQueues | Alec Faithfull | |
| 2015-10-09 | STM: Added functions for saving and restoring the internal state | Alec Faithfull | |
| PIDEtop needs these to implement its new transaction mechanism | |||
| 2015-10-09 | STM: Pass exception information to unreachable_state_hook functions | Alec Faithfull | |
| This lets hooks treat different exceptions in different ways; in particular, user interrupts can now be safely ignored | |||
| 2015-10-09 | Remove misleading warning (Close #4365) | Enrico Tassi | |
| 2015-10-08 | Univs: fix bug #3807 | Matthieu Sozeau | |
| Add a flag to disallow minimization to set | |||
| 2015-10-08 | Allowing empty bound universe variables. | Pierre-Marie Pédrot | |
| 2015-10-08 | Univs: fix bug #4161. | Matthieu Sozeau | |
| Retypecheck abstracted infered predicate to register the right universe constraints. | |||
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |