| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-03 | [vernac] mk_atts: an atts record with default values | Vincent Laporte | |
| 2018-07-03 | [vernac] attribute_of_flags | Vincent Laporte | |
| Elaborate a [atts] record out of a list of flags. | |||
| 2018-07-03 | Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands | Pierre-Marie Pédrot | |
| 2018-07-02 | Merge PR #7703: Add an option to force parameters to be uniform | Matthieu Sozeau | |
| 2018-07-02 | hints: add Hint Variables/Constants Opaque/Transparent commands | Matthieu Sozeau | |
| This gives user control on the transparent state of a hint db. Can override defaults more easily (report by J. H. Jourdan). For "core", declare that variables can be unfolded, but no constants (ensures compatibility with previous auto which allowed conv on closed terms) Document Hint Variables | |||
| 2018-07-02 | Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵ | Emilio Jesus Gallego Arias | |
| points of Camlp5 | |||
| 2018-07-01 | Add flag Uniform Inductive Parameters | Jasper Hugunin | |
| 2018-07-01 | Implement uniform parameters in ComInductive | Jasper Hugunin | |
| Don't allow notations attached to uniform inductives | |||
| 2018-07-01 | [api] Fix wrong deprecation warning (#7915) | Emilio Jesus Gallego Arias | |
| Fixes: #7915. Due to a change in the original misctypes removal PR, the deprecation notice went out of sync. | |||
| 2018-07-01 | Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation ↵ | Emilio Jesus Gallego Arias | |
| format). | |||
| 2018-07-01 | Merge PR #7759: Workaround to fix #7731 (printing not splitting line at ↵ | Emilio Jesus Gallego Arias | |
| break hint). | |||
| 2018-06-29 | Port g_vernac to the homebrew GEXTEND parser. | Pierre-Marie Pédrot | |
| 2018-06-29 | Port g_proofs to the homebrew GEXTEND parser. | Pierre-Marie Pédrot | |
| 2018-06-29 | Use a homebrew parser to replace the GEXTEND extension points of Camlp5. | Pierre-Marie Pédrot | |
| The parser is stupid and the syntax is almost the same as the previous one. The only difference is that one needs to wrap OCaml code between { braces } so that quoting works out of the box. Files requiring such a syntax are handled specifically by the type system and need to have a .mlg extension instead of a .ml4 one. | |||
| 2018-06-29 | Workaround to fix #7731 (printing not splitting line at break hint). | Hugo Herbelin | |
| In some cases, Format's inner boxes inside an outer box act as break hints, even though there are already "better" break hints in the outer box. We work around this "feature" by not inserting a box around the default printing rule for a notation if there is no effective break points in the box. See https://caml.inria.fr/mantis/view.php?id=7804 for the related OCaml discussion. | |||
| 2018-06-29 | Fixes #7712 (an anomaly in reporting bad recursive notation format). | Hugo Herbelin | |
| 2018-06-29 | Merge PR #7080: Swapping Context and Constr and defining declarations on ↵ | Maxime Dénès | |
| constr in Constr | |||
| 2018-06-28 | Make Environ.globals abstract. | Gaëtan Gilbert | |
| 2018-06-28 | Merge PR #7866: Implementation of mutual records in the higher strata | Maxime Dénès | |
| 2018-06-27 | Swapping Context and Constr: defining declarations on constr in Constr. | Hugo Herbelin | |
| This shall eventually allow to use contexts of declarations in the definition of the "Case" constructor. Basically, this means that Constr now includes Context and that the "t" types of Context which were specialized on constr are not defined in Constr (unfortunately using a heavy boilerplate). | |||
| 2018-06-27 | Merge PR #7863: Remove Sorts.contents | Pierre-Marie Pédrot | |
| 2018-06-26 | Merge PR #7906: universes_of_constr don't include universes of monomorphic ↵ | Pierre-Marie Pédrot | |
| constants | |||
| 2018-06-26 | Merge PR #7775: Fix handling of universe context for expanded program ↵ | Maxime Dénès | |
| obligations. | |||
| 2018-06-26 | Remove Sorts.contents | Gaëtan Gilbert | |
| 2018-06-26 | universes_of_constr don't include universes of monomorphic constants | Gaëtan Gilbert | |
| Apparently it was not useful. I don't remember what I was thinking when I added it. | |||
| 2018-06-25 | Merge PR #7798: Remove hack skipping comparison of algebraic universes in ↵ | Matthieu Sozeau | |
| subtyping. | |||
| 2018-06-25 | Merge PR #7559: Existing Class noop when already a class + warning. | Matthieu Sozeau | |
| 2018-06-24 | Further cleaning of the side-effect API. | Pierre-Marie Pédrot | |
| We remove internal functions and types from the API. | |||
| 2018-06-24 | Share the role type between the implementations of side-effects. | Pierre-Marie Pédrot | |
| We simply exploit a type isomorphism to remove the use of dedicated algebraic types in the kernel which are actually not necessary. | |||
| 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-22 | Fix handling of universe context for expanded program obligations. | Matthieu Sozeau | |
| The universe context was dropped even though it isn't added to the global universes yet. Keep it so that it is properly defined with the constant the expanded obligation appears in. | |||
| 2018-06-22 | Remove hack skipping comparison of algebraic universes in subtyping. | Gaëtan Gilbert | |
| When inferring [u <= v+k] I replaced the exception and instead add [u <= v]. This is trivially sound and it doesn't seem possible to have the one without the other (except specially for [Set <= v+k] which was already handled). I don't know an example where this used to fail and now succeeds (the point was to remove an anomaly, but the example ~~~ Module Type SG. Definition DG := Type. End SG. Module MG : SG. Definition DG := Type : Type. Fail End MG. ~~~ now fails with universe inconsistency. Fix #7695 (soundness bug!). | |||
| 2018-06-19 | Merge PR #7797: Remove reference name type. | Enrico Tassi | |
| 2018-06-19 | Merge PR #7801: [vernac] Add option to force building really mutual ↵ | Enrico Tassi | |
| induction schemes | |||
| 2018-06-18 | Remove reference name type. | Maxime Dénès | |
| reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid. | |||
| 2018-06-14 | Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ↵ | Pierre-Marie Pédrot | |
| of submodules. | |||
| 2018-06-13 | [vernac] Add option to force building really mutual induction schemes | Matthieu Sozeau | |
| Currently, if one of the inductives is non recursive, it defaults to a case analysis schems taking fewer predicates and methods just for that inductive. This irregularity prevents doing a combined scheme afterwards to gather all eliminators into one, as combined scheme expects all the eliminators to have the same predicates and methods. I have a use case in building function graphs in Equations where some of the inductives might not be recursive but I expect many other use cases could exist. | |||
| 2018-06-12 | [api] Add compatiblity Misctypes module. | Emilio Jesus Gallego Arias | |
| To be removed in 8.10. | |||
| 2018-06-12 | [api] Remove Misctypes. | Emilio Jesus Gallego Arias | |
| We move the last 3 types to more adequate places. | |||
| 2018-06-12 | [api] Misctypes removal: several moves: | Emilio Jesus Gallego Arias | |
| - move_location to proofs/logic. - intro_pattern_naming to Namegen. | |||
| 2018-06-12 | [api] Misctypes removal: miscellaneous aliases. | Emilio Jesus Gallego Arias | |
| 2018-06-08 | Existing Class noop when already a class + warning. | Gaëtan Gilbert | |
| Fix #5012. | |||
| 2018-06-07 | Merge PR #6874: [econstr] Some minor tweaks | Pierre-Marie Pédrot | |
| 2018-06-05 | Merge PR #7453: Refuse to parse empty [Context] command. | Matthieu Sozeau | |
| 2018-06-04 | Merge PR #7315: An attempt to clarify error message for Arguments needing ↵ | Maxime Dénès | |
| "rename" flag | |||
| 2018-06-04 | Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <- | Pierre-Marie Pédrot | |
| 2018-06-04 | [econstr] Remove some Unsafe.to_constr use. | Emilio Jesus Gallego Arias | |
| Most of it seems straightforward. | |||
| 2018-06-04 | [vernac] Switch back `auto_ind_decl` to Constr. | Emilio Jesus Gallego Arias | |
| AFAICT this tactic is always used on ground terms. | |||
| 2018-06-04 | Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode. | Matthieu Sozeau | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |