| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-07-08 | Similar purity invariants in the kernel. | Pierre-Marie Pédrot | |
| 2019-07-04 | Merge PR #10461: Simplify Declare.declare_variable | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego Reviewed-by: maximedenes Reviewed-by: ppedrot | |||
| 2019-07-04 | Merge PR #10359: Remove dependency of native_compile on global env for symbols | Maxime Dénès | |
| Reviewed-by: maximedenes Reviewed-by: ppedrot | |||
| 2019-07-03 | Safe_typing.push_named_assum: don't take universes | Gaëtan Gilbert | |
| The caller should push them first | |||
| 2019-06-27 | Kernel transparent definition entries have no body universes. | Gaëtan Gilbert | |
| 2019-06-26 | Perform the opaque section variable inference outside of the kernel. | Pierre-Marie Pédrot | |
| It is not the role of the kernel to decide to force the body of an entry to infer the section variable it uses, but the one of the upper layers. We make this explicit in the type of entries so as to enforce that this inference is performed beforehand. Also removes auxilliary file stuff that doesn't look like it belongs in the kernel either. | |||
| 2019-06-26 | Remove dead code for typing of section definitions in kernel. | Pierre-Marie Pédrot | |
| All section definitions are always defined as if they were transparent, all the additional checks were actually never triggered. | |||
| 2019-06-25 | Merge PR #10284: Expose set interface to option tables | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Reviewed-by: ejgallego Reviewed-by: ppedrot | |||
| 2019-06-24 | Code simplification for definition_entry type. | Pierre-Marie Pédrot | |
| 2019-06-24 | Remove the unused opaque_entry_inline_code field from opaque entries. | Pierre-Marie Pédrot | |
| 2019-06-24 | Enforce that opaque entries carry their type. | Pierre-Marie Pédrot | |
| 2019-06-24 | Dedicated type for opaque entries in the kernel. | Pierre-Marie Pédrot | |
| Even more invariants can be enforced this way. | |||
| 2019-06-24 | Enforce that transparent entries are forced beforehand. | Pierre-Marie Pédrot | |
| 2019-06-24 | Take advantage of the change of entry representation to split opacity status. | Pierre-Marie Pédrot | |
| Mere isomorphism for now, but will allow more invariants ultimately. | |||
| 2019-06-17 | Merge PR #10362: Kernel-side delaying of polymorphic opaque constants | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Reviewed-by: gares | |||
| 2019-06-17 | Update headers of files that were stuck on older headers. | Théo Zimmermann | |
| Most of these files were introduced after #6543 but used older headers copied from somewhere else. | |||
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann | |
| 2019-06-17 | Clean up the code adding monomorphic global constraints in Safe_typing. | Pierre-Marie Pédrot | |
| 2019-06-17 | Merge universe quantification and delayed constraints in opaque proofs. | Pierre-Marie Pédrot | |
| This enforces more invariants statically. | |||
| 2019-06-17 | Allow to delay polymorphic opaque constants. | Pierre-Marie Pédrot | |
| We had to move the private opaque constraints out of the constant declaration into the opaque table. The API is not very pretty yet due to a pervasive confusion between monomorphic global constraints and polymorphic local ones, but once we get rid of futures in the kernel this should be magically solved. | |||
| 2019-06-12 | Remove dependency of native_compile on global env for symbols | Gaëtan Gilbert | |
| Instead we get the symbols from a Environ.env. We make them accessible to the produced code through a reference managed by the kernel, similar to the return values except inverting when it's written and when it's read. | |||
| 2019-06-11 | Move the side-effect role out of Entries into Evd. | Pierre-Marie Pédrot | |
| 2019-06-11 | Remove the side-effect role from the kernel. | Pierre-Marie Pédrot | |
| We move the role data into the evarmap instead. | |||
| 2019-06-11 | Move type definition Nativecode.symbols to Nativevalues | Gaëtan Gilbert | |
| Preparing for it to be stored in an Environ.env. | |||
| 2019-06-07 | Merge PR #10308: Merge the two sources of monomorphic constraints for ↵ | Gaëtan Gilbert | |
| side-effects Reviewed-by: SkySkimmer | |||
| 2019-06-06 | Merge PR #9972: [build] Select uint63 using `ocamlc -config` variables. | Vincent Laporte | |
| Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Reviewed-by: gares Reviewed-by: maximedenes Reviewed-by: vbgl | |||
| 2019-06-06 | Merge the two sources of monomorphic constraints for side-effects. | Pierre-Marie Pédrot | |
| Instead of having the monormorphic universes from the immediate data separated from the ones from the body, we only rely on the former. There is no reason to delay given that the body is always force upfront. | |||
| 2019-06-04 | Remove the discharge segment from vo files. | Pierre-Marie Pédrot | |
| Since the introduction of delayed section substitution, the opaque table was already containing the same information. | |||
| 2019-06-04 | Slightly tweak the representation of dischargeable opaque proofs. | Pierre-Marie Pédrot | |
| This will allow an easier removal of the discharge segment in a later commit. | |||
| 2019-06-04 | Do not substitute opaque constants when discharging. | Pierre-Marie Pédrot | |
| Instead we do that on a by-need basis by reusing the section info already stored in the opaque proof. | |||
| 2019-06-03 | Expose set interface to option tables | Gaëtan Gilbert | |
| This lets us avoid having to cache the SearchBlacklist.elements call in search as we can just use the set module's for_all function. | |||
| 2019-05-31 | Fix #10268: vio2vo produces incorrect term when discharging. | Pierre-Marie Pédrot | |
| We do not partially abstract the section info. Instead, we reuse the same code in cook_constr and cook_constant and pass the same section info. | |||
| 2019-05-29 | Merge PR #10252: Various dynamic assertions and cleanups in opaque typing | Maxime Dénès | |
| Reviewed-by: SkySkimmer Reviewed-by: maximedenes Ack-by: ppedrot | |||
| 2019-05-29 | Merge PR #10248: Move the Discharge module in the kernel and merge it with ↵ | Maxime Dénès | |
| Cooking Reviewed-by: SkySkimmer Ack-by: herbelin Reviewed-by: maximedenes Ack-by: ppedrot | |||
| 2019-05-28 | Merge PR #10258: Remove the delayed universe table from object files. | Enrico Tassi | |
| Reviewed-by: SkySkimmer Reviewed-by: gares | |||
| 2019-05-28 | Merge PR #10133: mind_kelim is the highest allowed sort instead of a list | Pierre-Marie Pédrot | |
| Ack-by: maximedenes Reviewed-by: ppedrot | |||
| 2019-05-27 | Remove the delayed universe table from object files. | Pierre-Marie Pédrot | |
| This was virtually dead code. The only place really accessing this data was the user pretty-printer, but actually the tables were not installed for vanilla vo files. In practice, that meant that the only case where an access to this table could have been triggered would have been to print a term coming from a vio file, or a vo file generated via vio2vo. In all other cases, the printer would not have displayed the internal universes. While the latter might be considered a bug, I am instead convinced that this notion of user-facing internal universes needs to be handled by another mechanism, the current one making little sense. The fact it was broken all along without anybody noticing proves my point. | |||
| 2019-05-27 | Merge PR #10249: More precise type for export and inlining of private constants | Maxime Dénès | |
| Reviewed-by: gares Ack-by: maximedenes | |||
| 2019-05-27 | Fix #10251: Type-checking of polymorphic opaque constr entry types is broken. | Pierre-Marie Pédrot | |
| We use the right environment. | |||
| 2019-05-27 | Specific code path for opaque polymorphic constants. | Pierre-Marie Pédrot | |
| For now this is just a specialized version of the previous generic code. This simplifies tracking of the changes. | |||
| 2019-05-27 | Ensure dynamically that non-opaque definitions are always side-effect free. | Pierre-Marie Pédrot | |
| It is guaranteed by Declare, but a little dynamic check does not hurt. | |||
| 2019-05-27 | Ensure dynamically that opaque definitions come with their type. | Pierre-Marie Pédrot | |
| The only lawbreaker was the Add Ring command. We generate a type for the declaration to fix the code. | |||
| 2019-05-27 | mind_kelim is the highest allowed sort instead of a list | Gaëtan Gilbert | |
| 2019-05-26 | More precise type for Safe_typing export and inlining of private constants. | Pierre-Marie Pédrot | |
| We get rid of the future wrappers, as all callers are immediately forcing the result. | |||
| 2019-05-26 | Code sharing inside Cooking. | Pierre-Marie Pédrot | |
| 2019-05-26 | Actually merge Discharge into Cooking. | Pierre-Marie Pédrot | |
| This is the intended module for the feature provided by the inductive discharge. This allows for a bit of code sharing and cleanup. | |||
| 2019-05-26 | Share API between Discharge and Cooking. | Pierre-Marie Pédrot | |
| 2019-05-26 | Move the Discharge module into the kernel. | Pierre-Marie Pédrot | |
| 2019-05-25 | Centralize the hashconsing of constant declarations. | Pierre-Marie Pédrot | |
| Safe_typing is now responsible for hashconsing of all accessible structures, except for opaque terms which are handled by Opaqueproof. | |||
| 2019-05-24 | Merge PR #10233: Fixing typos - Part 3 | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |