| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-06-03 | Merge PR #10277: Remove Show Script (deprecated in 8.10) | Théo Zimmermann | |
| Reviewed-by: Zimmi48 Reviewed-by: gares | |||
| 2019-06-03 | Merge PR #10261: Update doc to reflect that PG now supports Coq-generated ↵ | Théo Zimmermann | |
| proof diffs Reviewed-by: Zimmi48 Reviewed-by: cpitclaudel Ack-by: erikmd | |||
| 2019-06-03 | Update doc to reflect that PG now supports Coq-generated proof diffs | Jim Fehrle | |
| 2019-05-31 | Remove Show Script (deprecated in 8.10) | Gaëtan Gilbert | |
| 2019-05-30 | Merge PR #10269: Checker: don't use monomorphic universes attached to a constant | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 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-29 | Merge PR #10270: Fix debug printers | Enrico Tassi | |
| Reviewed-by: gares | |||
| 2019-05-29 | Merge PR #10049: [elaboration] Bidirectionality hints | Enrico Tassi | |
| Ack-by: RalfJung Reviewed-by: SkySkimmer Reviewed-by: gares Ack-by: maximedenes | |||
| 2019-05-28 | Merge PR #10228: gitlab: run less jobs unless FULL_CI=true | Emilio Jesus Gallego Arias | |
| Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego | |||
| 2019-05-28 | Fix printers.sh test when missing coqtop.byte, print more info | Gaëtan Gilbert | |
| 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 | Fix [Drop. #use "include";;] for indirect_accessor | Gaëtan Gilbert | |
| 2019-05-28 | [elaboration] Bidirectionality hints | Maxime Dénès | |
| This feature makes it possible to tell type inference to type applications of a global `foo` using typing information from the context once the `n` first arguments are known. The syntax is: `Arguments foo x y | z`. Closes #7910 | |||
| 2019-05-28 | Same universe constraint fix for the checker. | Pierre-Marie Pédrot | |
| 2019-05-28 | Checker: don't use monomorphic universes attached to a constant | Gaëtan Gilbert | |
| They are supposed to be included in the module's constraints. The old behaviour would allow a crafted vo, using ~~~coq Definition a := Type. Definition b := Type. Definition b_in_a : a := b. Definition a_in_b : b := a. ~~~ with the constraints for b_in_a and a_in_b not included in the module constraints, then a proof of false may be derived in the usual way. | |||
| 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 | gitlab: run less jobs unless FULL_CI=true | Gaëtan Gilbert | |
| The idea is that it's unlikely for only 1 of the test suite copies to fail for a real reason, so we don't need to run all of them. I would prefer to have only 1 build stage job but later stages depend on build:base, build:edge+flambda and build:edge+flambda:dune:dev for non-copy-pasted jobs. I kept corresponding test suite and validate job copies but they could also be filtered. | |||
| 2019-05-27 | Overlay for mind_kelim change (#10133) | Gaëtan Gilbert | |
| 2019-05-27 | mind_kelim is the highest allowed sort instead of a list | Gaëtan Gilbert | |
| 2019-05-27 | Merge PR #10241: Update README.md / add SUPPORT.md file. | Maxime Dénès | |
| Reviewed-by: maximedenes | |||
| 2019-05-27 | Merge PR #10198: Centralize the hashconsing of constant declarations. | Maxime Dénès | |
| Reviewed-by: maximedenes | |||
| 2019-05-27 | Merge PR #10235: [debug] Print restriction metadata in evar map debug printer | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2019-05-27 | Merge PR #10237: Fix some incorrect uses of proof-local environment | Pierre-Marie Pédrot | |
| Reviewed-by: gares Reviewed-by: ppedrot | |||
| 2019-05-27 | [debug] Print restriction metadata in evar map debug printer | Maxime Dénès | |
| 2019-05-26 | Merge PR #10220: Use new coqrst syntax for alternatives in SSReflect chapter. | Enrico Tassi | |
| Reviewed-by: gares | |||
| 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 | Merge PR #10244: Coqc: Treat unknown arguments starting with dash as unknown ↵ | Emilio Jesus Gallego Arias | |
| options rather than files Reviewed-by: ejgallego | |||
| 2019-05-25 | Merge PR #9288: Giving preference to syntax "injection ... as [= pat1 ... ↵ | Théo Zimmermann | |
| patn]". Reviewed-by: Zimmi48 | |||
| 2019-05-25 | Coqc: Treat unknown arguments starting with dash as unknown options rather ↵ | Hugo Herbelin | |
| than files. | |||
| 2019-05-25 | Modifying theories to preferably use the "[= ]" syntax, and, | Hugo Herbelin | |
| sometimes, to use "intros [= ...]" rather than things like "intros H; injection H as [= ...]". Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | |||
| 2019-05-25 | Documenting syntax "injection ... as [= pat1 ... patn ]". | Hugo Herbelin | |
| To prevent confusion, forbidding a mix of the "injection term as pat1 ... patn" and of the "injection term as [= pat1 ... patn]" syntax: If a "[= ...]" occurs, this should be a singleton list of patterns. | |||
| 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 | Add SUPPORT.md file. | Théo Zimmermann | |
| A link to this file will be displayed when people start opening an issue, and maybe in some other places. See also: https://help.github.com/en/articles/adding-support-resources-to-your-project | |||
| 2019-05-24 | Update README, remove MacPorts link (not updated since 8.8.2). | Théo Zimmermann | |
| 2019-05-24 | Merge PR #10233: Fixing typos - Part 3 | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-05-24 | Use global env in numeral and string notations | Maxime Dénès | |
| Since their introduction, these notations were incorrectly using the proof-local environment. | |||
| 2019-05-24 | Stop using pstate in global print queries | Gaëtan Gilbert | |
| Using pstate makes no sense for printing global stuff | |||
| 2019-05-24 | Merge PR #10209: Fix #10208 don't fail when passed extensionless -topfile | Enrico Tassi | |
| Reviewed-by: ppedrot | |||
| 2019-05-24 | Merge PR #10201: Remove access to indirect opaques in the kernel | Enrico Tassi | |
| Ack-by: SkySkimmer Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: maximedenes | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |