| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Merge branch 'v8.5' |  Pierre-Marie Pédrot | 2015-10-29 |
| |\ | |||
| | * | Avoid type checking private_constants (side_eff) again during Qed (#4357). |  Enrico Tassi | 2015-10-28 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Side effects are now an opaque data type, called private_constant, you can only obtain from safe_typing. When add_constant is called on a definition_entry that contains private constants, they are either - inlined in the main proof term but not re-checked - declared globally without re-checking them As a safety measure, the opaque data type contains a pointer to the revstruct (an internal field of safe_env that changes every time a new constant is added), and such pointer is compared with the current value store in safe_env when the private_constant is inlined. Only when the comparison is successful the private_constant is not re-checked. Otherwise else it is. In short, we accept into the kernel private constant only when they arrive in the very same order and on top of the very same env they arrived when we fist checked them. Note: private_constants produced by workers never pass the safety measure (the revstruct pointer is an Ephemeron). Sending back the entire revstruct is possible but: 1. we lack a way to quickly compare two revstructs, 2. it can be large. | ||
| * | | Opacifying the proof_terminator type. | Pierre-Marie Pédrot | 2015-09-08 |
| |/ | |||
| * | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi | 2015-03-11 |
| | | | | | | | | | | | | | | | | - 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 | ||
| * | Fixing OCaml 3.12 compilation. | Pierre-Marie Pédrot | 2015-02-14 |
| | | |||
| * | Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior | Enrico Tassi | 2015-02-14 |
| | | | | | Of course such proofs cannot be processed asynchronously | ||
| * | Update headers. |  Maxime Dénès | 2015-01-12 |
| | | |||
| * | Avoiding introducing yet another convention in naming files. |  Hugo Herbelin | 2015-01-08 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |