| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-05-10 | [Canonical structures] “not_canonical” annotation to field declarations | Vincent Laporte | |
| 2019-05-10 | [Canonical structures] Some projections may not be canonical | Vincent Laporte | |
| 2019-05-07 | [Record] Une a record to gather field declaration attributes | Vincent Laporte | |
| 2019-05-07 | [Record] Deforestation | Vincent Laporte | |
| 2019-04-10 | Remove calls to Global.env and Libobject from Recordops | Maxime Dénès | |
| 2019-04-10 | Functionalize env in type classes | Maxime Dénès | |
| I had to reorganize the code a bit. The Context command moved to comAssumption, as it is not so related to type classes. We were able to remove a few hooks on the way. | |||
| 2019-03-30 | [Canonical structures] Minor refactoring | Vincent Laporte | |
| 2019-03-14 | Repair relevance marks in-kernel. | Gaëtan Gilbert | |
| Prevent errors when under annotating binders. | |||
| 2019-03-14 | Inductives in SProp, forbid primitive records with only sprop fields | Gaëtan Gilbert | |
| For nonsquashed: Either - 0 constructors - primitive record | |||
| 2019-03-14 | Add relevance marks on binders. | Gaëtan Gilbert | |
| Kernel should be mostly correct, higher levels do random stuff at times. | |||
| 2019-03-14 | Make Sorts.t private | Gaëtan Gilbert | |
| 2019-03-12 | Merge PR #9596: Fix #9595: missing non-primitive-record warning with 0 field ↵ | Emilio Jesus Gallego Arias | |
| record Reviewed-by: ejgallego | |||
| 2019-02-28 | Implement a method for manual declaration of implicits. | Jasper Hugunin | |
| This is intended to be separate from handling of implicit binders. The remaining uses of declare_manual_implicits satisfy a lot of assertions, giving the possibility of simplifying the interface in the future. Two disabled warnings are added for things that currently pass silently. Currently only Mtac passes non-maximal implicits to declare_manual_implicits with the force-usage flag set. When implicit arguments don't have to be named, should move Mtac over to set_implicits. | |||
| 2019-02-19 | Fix #9595: missing non-primitive-record warning with 0 field record | Gaëtan Gilbert | |
| 2019-02-17 | Separate variance and universe fields in inductives. | Gaëtan Gilbert | |
| I think the usage looks cleaner this way. | |||
| 2019-02-08 | Merge PR #9410: Make `Program` a regular attribute | Matthieu Sozeau | |
| Ack-by: SkySkimmer Reviewed-by: aspiwack Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: mattam82 Ack-by: maximedenes | |||
| 2019-02-05 | Merge PR #9373: Kernel: don't automatically downgrade ill-shaped primitive ↵ | Pierre-Marie Pédrot | |
| records Reviewed-by: ppedrot | |||
| 2019-02-05 | Make Program a regular attribute | Maxime Dénès | |
| We remove all calls to `Flags.is_program_mode` except one (to compute the default value of the attribute). Everything else is passed explicitely, and we remove the special logic in the interpretation loop to set/unset the flag. This is especially important since the value of the flag has an impact on proof modes, so on the separation of parsing and execution phases. | |||
| 2019-02-04 | Merge PR #9317: Restrict universes in records. | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Reviewed-by: mattam82 Reviewed-by: ppedrot | |||
| 2019-01-30 | Restrict universes in records. | Gaëtan Gilbert | |
| Fix #8076. | |||
| 2019-01-25 | Move non-primitive-record warning to declare_mutual_inductive_with_eliminations | Gaëtan Gilbert | |
| This makes it print the warning before the definition message, so if we run with +non-primitive-record we don't see """ defined foo error could not define foo """ | |||
| 2019-01-24 | Kernel: don't automatically downgrade ill-shaped primitive records | Gaëtan Gilbert | |
| This simplifies reasoning about the kernel code. We still auto downgrade squashed Prop records as the code path to avoid an error is more involved. Alternatively we could produce an error forcing people to Unset Primitive Projections if they want a squashed record. | |||
| 2018-12-19 | warn when using auto template, funind never uses template poly | Gaëtan Gilbert | |
| The warning can be avoided with the attributes, (or just disable the warning itself I guess). | |||
| 2018-12-09 | [doc] Enable Warning 50 [incorrect doc comment] and fix comments. | Emilio Jesus Gallego Arias | |
| This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :) | |||
| 2018-11-28 | Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a class | Matthieu Sozeau | |
| 2018-11-27 | Merge PR #9046: Goptions.declare_* functions return unit instead of a ↵ | Emilio Jesus Gallego Arias | |
| write_function | |||
| 2018-11-27 | Record.declare_class: remove unused “finite” parameter | Vincent Laporte | |
| 2018-11-23 | s/let _ =/let () =/ in some places (mostly goptions related) | Gaëtan Gilbert | |
| 2018-11-21 | Make initial evar map argument to check_evars_are_solved optional. | Gaëtan Gilbert | |
| (same for solve_remaining_evars) This is the standard way to use these functions, with 1 exception in Unification. | |||
| 2018-11-09 | Remove remnants of polymorphic instance name registration. | Pierre-Marie Pédrot | |
| 2018-11-09 | Force the user to provide names when generating abstract universe contexts. | Pierre-Marie Pédrot | |
| For now this data is not stored, but the code checks that indeed the number of names provided coincide with the instance length. I had to reimplement the same kind of workaround hack in section handling as the one already performed in UnivNames because the name information is not present in the section data structure. This deserves a FIXME. | |||
| 2018-11-09 | Adding universe names to polymorphic entry instances. | Pierre-Marie Pédrot | |
| 2018-10-26 | Merge PR #8684: Remove a few circumvolutions around parameters of inductive ↵ | Gaëtan Gilbert | |
| entries | |||
| 2018-10-26 | Remove a few circumvolutions around parameters of inductive entries | Maxime Dénès | |
| 2018-10-19 | Deprecating Global.type_of_global_in_context. | Hugo Herbelin | |
| Removing a few Global.env in the way. | |||
| 2018-09-19 | Fix #7754: universe declarations on mutual inductives | Gaëtan Gilbert | |
| 2018-09-19 | Merge PR #8341: Reduce universe redeclarations (catching AlreadyDeclared) | Matthieu Sozeau | |
| 2018-09-13 | Do not redeclare universes for monomorphic operational typeclasses | Gaëtan Gilbert | |
| eg in [Class Foo (A:Type) := foo : A.] the universe should be declared when declaring the constant [Foo] and not [foo]. | |||
| 2018-09-13 | Add option to control automatic template polymorphism. | Gaëtan Gilbert | |
| 2018-09-13 | Add explicit atribute for template polymorphism. | Gaëtan Gilbert | |
| 2018-09-13 | Elaboration: do not ask for small records to be template | Gaëtan Gilbert | |
| Imitating the kernel in anticipation for the kernel being more obedient | |||
| 2018-07-24 | Projections use index representation | Gaëtan Gilbert | |
| The upper layers still need a mapping constant -> projection, which is provided by Recordops. | |||
| 2018-06-28 | Merge PR #7866: Implementation of mutual records in the higher strata | Maxime Dénès | |
| 2018-06-26 | Remove Sorts.contents | Gaëtan Gilbert | |
| 2018-06-25 | Merge PR #7559: Existing Class noop when already a class + warning. | Matthieu Sozeau | |
| 2018-06-24 | Handle mutual record at the vernac level. | Pierre-Marie Pédrot | |
| Highly spaghetti code, hopefully works. | |||
| 2018-06-23 | Using more general information for primitive records. | Pierre-Marie Pédrot | |
| This brings more compatibility with handling of mutual primitive records in the kernel. | |||
| 2018-06-12 | [api] Misctypes removal: several moves: | Emilio Jesus Gallego Arias | |
| - move_location to proofs/logic. - intro_pattern_naming to Namegen. | |||
| 2018-06-08 | Existing Class noop when already a class + warning. | Gaëtan Gilbert | |
| Fix #5012. | |||
| 2018-05-31 | [api] Move `Constrexpr` to the `interp` module. | Emilio Jesus Gallego Arias | |
| Continuing the interface cleanup we place `Constrexpr` in the internalization module, which is the one that eliminates it. This slims down `pretyping` considerably, including removing the `Univdecls` module which existed only due to bad dependency ordering in the first place. Thanks to @ Skyskimmer we also remove a duplicate `univ_decl` definition among `Misctypes` and `UState`. This is mostly a proof of concept yet as it depends on quite a few patches of the tree. For sure some tweaks will be necessary, but it should be good for review now. IMO the tree is now in a state where we can could easy eliminate more than 10 modules without any impact, IMHO this is a net saving API-wise and would help people to understand the structure of the code better. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |