| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-03-15 | STM: -quick: async no Proof using but no Section (#4124) | Enrico Tassi | |
| As happens in interactive mode. | |||
| 2015-03-14 | End of Bug 3986 - make cleanall removes .*.aux files | Pierre Boutillier | |
| 2015-03-14 | Bug 3981 ends to convice me that subdirs in coq_makefile deverse a warning | Pierre Boutillier | |
| 2015-03-14 | Fix Bug 3548 - Makefile should fallback gracefully in the absence of codesign | Pierre Boutillier | |
| 2015-03-13 | Fix compilation with forthcoming Ocaml version 4.03. | Arnaud Spiwack | |
| Backported from a patch for v8.4 by Pierre Chambart. Part of the commit has been rendered obsolete by code reorganisation, leaving: * OCaml runtime header files used to declare the int32, uint32, int64 and uint64 type. That got removed, and uses of those types should be replaced by the standard ones: uint32_t, int32_t, int64_t, uint64_t. Those are defined in stdint.h. | |||
| 2015-03-13 | Declarative mode: make it so that unfocussing can only be done for closed ↵ | Arnaud Spiwack | |
| subproofs. The front-end is supposed to take care of that, but it may help to catch bugs. | |||
| 2015-03-13 | Declarative mode: remove dead code. | Arnaud Spiwack | |
| 2015-03-13 | Declarative mode: remove a superfluous [set_proof_mode]. | Arnaud Spiwack | |
| It was probably creating bugs when trying to use [escape]. | |||
| 2015-03-13 | Declarative mode: fix the focus behaviour. | Arnaud Spiwack | |
| I had previously mistakenly enforced the property that after solving every goal in a block, unfocusing was performed automatically until one goal is in focus. This is not how the declarative mode is supposed to behave. Rather every focus must be explicitely unfocused by a closing command. This hit a few bad interaction with the pure representation of proof introduced for the asynchronous processing. Some of the invariants seem fragile, so this minimally disruptive solution is probably not long-term. In particular since each block uses the same focus kind, an `end <block>` may close another block than intended if the number of unfocussing command executed is not the right one. | |||
| 2015-03-13 | rewiring Czar printers that were disabled | Pierre Corbineau | |
| Backported from trunk. | |||
| 2015-03-13 | CHANGES: more correct equivalent to "constructor tac" syntax. | Arnaud Spiwack | |
| As mentionne in #3969, using "once (constructor;tac)" leads in exponential blowups, whereas "[> once (constructor;tac) ..]" does not. | |||
| 2015-03-13 | Add some tests for tryif | Jason Gross | |
| + adjusting for the removal of `admit` by Arnaud Spiwack. | |||
| 2015-03-13 | Fixing #4127 (command for locating exists notation in refman changed). | Hugo Herbelin | |
| 2015-03-12 | Fixing bug #4055. | Pierre-Marie Pédrot | |
| When lauching ideslave without configuring the communication channels, instead of raising an anomaly which is never caught by the main loop, we rather exit the process with a relevant error message. | |||
| 2015-03-11 | Fix double print in decl_mode. | Enrico Tassi | |
| After executing a command classified as VtProofStep the stm prints the goals (if used via the tty API). | |||
| 2015-03-11 | Fix regression in HoTT_coq_014.v | Enrico Tassi | |
| Admitted was not using the partial proof to infer discharged variables. Now it does. The fix makes no sense, but restore the old behavior. | |||
| 2015-03-11 | CoqIDE: load first _CoqProject file found and notify the user | Enrico Tassi | |
| 2015-03-11 | CoqIDE: fix tag colors to support superposing unsafe and partial | Enrico Tassi | |
| Admitted (like Qed) can be "partially executed", but is also unsafe. | |||
| 2015-03-11 | CoqIDE: restore module/proof name in info bar | Enrico Tassi | |
| 2015-03-11 | CoqIDE: do not lose tag on Qed ending focused proof | Enrico Tassi | |
| 2015-03-11 | STM: ease re-editing of Admitted proofs | Enrico Tassi | |
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi | |
| - no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit | |||
| 2015-03-09 | Do not display the status of monomorphic constants unless in ↵ | Guillaume Melquiond | |
| universe-polymorphism mode. | |||
| 2015-03-08 | Test for bug #2951. | Pierre-Marie Pédrot | |
| 2015-03-08 | Fixing bug #2951. | Pierre-Marie Pédrot | |
| 2015-03-07 | Test for #4035 (dependent destruction from Ltac). | Hugo Herbelin | |
| 2015-03-07 | Reverting r10021 which enforces early assumptions on freshness which | Hugo Herbelin | |
| seem to be overly strong in practice (see discussion related to #4035). | |||
| 2015-03-07 | Continuing a8ad3abc15a2 and 60810aaec on freshness of name in tactic "evar". | Hugo Herbelin | |
| Not inventing a new fresh name if a non-fresh name is explicitly given, as in v8.4. | |||
| 2015-03-06 | Add some missing Proof keywords. | Guillaume Melquiond | |
| 2015-03-06 | Simplify grammar for syntax highlighting by removing extraneous parentheses. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Print/Reset Extraction. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Extraction Inline and add Separate Extraction. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Extraction Language. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Typeclasses Opaque. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Module (Type). | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Extract Inductive. | Guillaume Melquiond | |
| 2015-03-06 | Add syntax highlighting for Declare Module. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Import and Export. | Guillaume Melquiond | |
| 2015-03-06 | Add syntax highlighting for Declare ML Module. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Require. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Scheme. | Guillaume Melquiond | |
| 2015-03-06 | Do not highlight "using" as a constr keyword. | Guillaume Melquiond | |
| 2015-03-06 | Add syntax highlighting for About. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Save. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Hypothesis, Axiom, Variable, Parameter, and Context. | Guillaume Melquiond | |
| 2015-03-06 | Add syntax highlighting for Coercion. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of "Require multiple libraries". | Guillaume Melquiond | |
| 2015-03-06 | MMapPositive: another implementation of MMaps | Pierre Letouzey | |
| 2015-03-05 | Fix testsuite with respect to the new formatting of Fail messages. | Guillaume Melquiond | |
| 2015-03-05 | Preprend Fail to all the expected failures in the documentation. | Guillaume Melquiond | |
| This commit also removes comments from Coq examples, as they cause extraneous delayed prompts that clutter the output because coq_tex cannot remove them. Some documentation errors were also fixed in the process, since they are easier to spot now that only unexpected failures stand out. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |