| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-31 | Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name | Maxime Dénès | |
| 2017-08-30 | Fixing a capitalization in the middle of the sentence of an error message. | Hugo Herbelin | |
| 2017-08-29 | [vernac] Store Infix Modifier in Vernac Notation. | Pierre-Marie Pédrot | |
| This removes a dependency from `G_vernac` to `Metasyntax`. | |||
| 2017-08-29 | Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170 | Maxime Dénès | |
| 2017-08-29 | Merge PR #946: Functional pretyping interface | Maxime Dénès | |
| 2017-08-29 | Quoting notations in incompatible-level error message. | Hugo Herbelin | |
| 2017-08-29 | A new step of restructuration of notations. | Hugo Herbelin | |
| This allows to issue a more appropriate message when a notation with a { } cannot be defined because of an incompatible level. E.g.: Notation "{ A } + B" := (sumbool A B) (at level 20). | |||
| 2017-08-29 | Dropping former fix to bug #5469 (notation format not recognizing curly braces). | Hugo Herbelin | |
| This reverts commit 53a50875 and a bit more: it also makes the check for possibly ignoring formatting spaces irrelevant, since the previous commit makes that curly brackets are not any more dropped for printing. | |||
| 2017-08-29 | A little reorganization of notations + a fix to #5608. | Hugo Herbelin | |
| - Formerly, notations such as "{ A } + { B }" were typically split into "{ _ }" and "_ + _". We keep the split only for parsing, which is where it is really needed, but not anymore for interpretation, nor printing. - As a consequence, one notation string can give rise to several grammar entries, but still only one printing entry. - As another consequence, "{ A } + { B }" and "A + { B }" must be reserved to be used, which is after all the natural expectation, even if the sublevels are constrained. - We also now keep the information "is ident", "is binder" in the "key" characterizing the level of a notation. | |||
| 2017-08-29 | Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map | Hugo Herbelin | |
| (from module List). | |||
| 2017-08-17 | Add native compute profiling, BZ#5170 | Paul Steckler | |
| 2017-08-16 | Merge PR #912: Detyping functions are now operating on EConstr.t. | Maxime Dénès | |
| 2017-08-16 | Merge PR #841: Timorous fix of bug #5598 on global existing class in sections | Maxime Dénès | |
| 2017-08-16 | Merge PR #864: Some cleanups after cumulativity for inductive types | Maxime Dénès | |
| 2017-08-01 | Remove understand_tcc_evars. | Maxime Dénès | |
| Use the functional interface understand_tcc instead. | |||
| 2017-08-01 | Detyping functions are now operating on EConstr.t. | Pierre-Marie Pédrot | |
| This was already the case, but the API was not exposing this. | |||
| 2017-08-01 | Merge PR #919: Remove a few useless evar-normalizations in printing code. | Maxime Dénès | |
| 2017-08-01 | Merge PR #834: Adding support for recursive notations of the form "x , .. , ↵ | Maxime Dénès | |
| y , z". | |||
| 2017-07-31 | Improve errors for cumulativity when monomorphic | Amin Timany | |
| We now only issue an error for locally specified (non)cumulativity whenever it is the context (set locally or globally) is monorphic. | |||
| 2017-07-31 | Change the option for cumulativity | Amin Timany | |
| 2017-07-31 | Issue error on monomorphic cumulative inductives | Amin Timany | |
| 2017-07-31 | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead | Maxime Dénès | |
| 2017-07-27 | deprecate Pp.std_ppcmds type alias | Matej Košík | |
| 2017-07-26 | Remove a few useless evar-normalizations in printing code. | Pierre-Marie Pédrot | |
| 2017-07-26 | Removing template polymorphism for definitions. | Pierre-Marie Pédrot | |
| The use of template polymorphism in constants was quite limited, as it only applied to definitions that were exactly inductive types without any parameter whatsoever. Furthermore, it seems that following the introduction of polymorphic definitions, the code path enforced regular polymorphism as soon as the type of a definition was given, which was in practice almost always. Removing this feature had no observable effect neither on the test-suite, nor on any development that we monitor on Travis. I believe it is safe to assume it was nowadays useless. | |||
| 2017-07-26 | Statically ensuring that inlined entries out of the kernel have no effects. | Pierre-Marie Pédrot | |
| This was an easy to prove property that I somehow overlooked. | |||
| 2017-07-26 | More precise type for universe entries. | Pierre-Marie Pédrot | |
| We use an algebraic type instead of a pair of a boolean and the corresponding data. For now, this is isomorphic, but this allows later change in the structure. | |||
| 2017-07-26 | Adding support for recursive notations of the form "x , .. , y , z". | Hugo Herbelin | |
| Since camlp5 parses from left, the last ", z" was parsed as part of an arbitrary long list of "x1 , .. , xn" and a syntax error was raised since an extra ", z" was still expected. We support this by translating "x , .. , y , z" into "x , y , .. , z" and reassembling the arguments appropriately after parsing. | |||
| 2017-07-20 | Merge PR #899: [general] Move files to directories so they match linking order. | Maxime Dénès | |
| 2017-07-20 | Merge branch 'v8.7' | Maxime Dénès | |
| 2017-07-19 | Merge PR #770: [proof] Move bullets to their own module. | Maxime Dénès | |
| 2017-07-19 | [general] Move files to directories matching linking order. | Emilio Jesus Gallego Arias | |
| We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`, `Miscprint`) to their proper place as they were declared in different `mllib` files than the one in their directory. In some cases this could be refined but we don't do anything fancy, we just reflect the status quo. | |||
| 2017-07-17 | Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers | Maxime Dénès | |
| 2017-07-17 | Merge PR #862: Adding support for bindings tags to explicit prefix/suffix ↵ | Maxime Dénès | |
| rather than colors | |||
| 2017-07-13 | Removing the uses of abstraction-breaking code in Lemmas. | Pierre-Marie Pédrot | |
| I had to slightly tweak a test in order to work around a bug of simpl that loses universes constraints when refolding polymorphic fixpoints. | |||
| 2017-07-13 | Removing the uses of abstraction-breaking code in Obligations. | Pierre-Marie Pédrot | |
| 2017-07-13 | Remove the function Global.type_of_global_unsafe. | Pierre-Marie Pédrot | |
| 2017-07-13 | The only abstraction-breaking function in Univ is now AUContext.instance. | Pierre-Marie Pédrot | |
| 2017-07-13 | Getting rid of AUContext abstraction breakers in Discharge. | Pierre-Marie Pédrot | |
| 2017-07-13 | Make the typeclass implementation fully compatible with universe polymorphism. | Pierre-Marie Pédrot | |
| This essentially means storing the abstract universe context in the typeclass data, and abstracting it when necessary. | |||
| 2017-07-13 | Safer API for Global.body_of_constant and variants. | Pierre-Marie Pédrot | |
| We aditionally return the abstract universe context inside the option. This is relatively painless as most uses were using the option as a boolean. | |||
| 2017-07-13 | Safer API for Global.type_of_global_in_context. | Pierre-Marie Pédrot | |
| We return the abstract context instead of an arbitrary instantiation. | |||
| 2017-07-13 | Getting rid of AUContext abstraction breakers in Record. | Pierre-Marie Pédrot | |
| 2017-07-13 | Getting rid of AUContext abstraction breakers in Search. | Pierre-Marie Pédrot | |
| 2017-07-11 | Deprecate options that were introduced for compatibility with 8.5. | Théo Zimmermann | |
| 2017-07-11 | Properly handling polymorphic inductive subtyping in the kernel. | Pierre-Marie Pédrot | |
| Before this patch, inductive subtyping was enforcing syntactic equality of the variable instance, instead of reasoning up to alpha-renaming. | |||
| 2017-07-11 | Safe API for accessing universe constraints of global references. | Pierre-Marie Pédrot | |
| Instead of returning either an instance or the set of constraints, we rather return the corresponding abstracted context. We also push back all uses of abstraction-breaking calls from these functions out of the kernel. | |||
| 2017-07-08 | Adding support for bindings tags to explicit prefix/suffix rather than colors. | Hugo Herbelin | |
| This is usable for no-color terminal. For instance, a typical application in mind is the Coq-generate names marker which can be rendered with a color if the interface supports it and a prefix "~" if the interface does not support colors. | |||
| 2017-07-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |