aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
Commit message (Collapse)AuthorAge
...
* | | | | A little reorganization of notations + a fix to #5608.Gravatar Hugo Herbelin2017-08-29
| |_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - 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.
| | | * Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_mapGravatar Hugo Herbelin2017-08-29
| |_|/ |/| | | | | | | | (from module List).
| | * Add native compute profiling, BZ#5170Gravatar Paul Steckler2017-08-17
| |/ |/|
* | Merge PR #912: Detyping functions are now operating on EConstr.t.Gravatar Maxime Dénès2017-08-16
|\ \
* \ \ Merge PR #841: Timorous fix of bug #5598 on global existing class in sectionsGravatar Maxime Dénès2017-08-16
|\ \ \
* \ \ \ Merge PR #864: Some cleanups after cumulativity for inductive typesGravatar Maxime Dénès2017-08-16
|\ \ \ \
| | | | * Remove understand_tcc_evars.Gravatar Maxime Dénès2017-08-01
| |_|_|/ |/| | | | | | | | | | | Use the functional interface understand_tcc instead.
| | | * Detyping functions are now operating on EConstr.t.Gravatar Pierre-Marie Pédrot2017-08-01
| |_|/ |/| | | | | | | | This was already the case, but the API was not exposing this.
* | | Merge PR #919: Remove a few useless evar-normalizations in printing code.Gravatar Maxime Dénès2017-08-01
|\ \ \
* \ \ \ Merge PR #834: Adding support for recursive notations of the form "x , .. , ↵Gravatar Maxime Dénès2017-08-01
|\ \ \ \ | | | | | | | | | | | | | | | y , z".
| | | * | Improve errors for cumulativity when monomorphicGravatar Amin Timany2017-07-31
| | | | | | | | | | | | | | | | | | | | | | | | | We now only issue an error for locally specified (non)cumulativity whenever it is the context (set locally or globally) is monorphic.
| | | * | Change the option for cumulativityGravatar Amin Timany2017-07-31
| | | | |
| | | * | Issue error on monomorphic cumulative inductivesGravatar Amin Timany2017-07-31
| | | | |
* | | | | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \ \ \ \ | |_|_|/ / |/| | | |
| * | | | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| | | | |
| | | * | Remove a few useless evar-normalizations in printing code.Gravatar Pierre-Marie Pédrot2017-07-26
| | |/ / | |/| |
* | | | Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | Statically ensuring that inlined entries out of the kernel have no effects.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | | | | | | | | | This was an easy to prove property that I somehow overlooked.
* | | | More precise type for universe entries.Gravatar Pierre-Marie Pédrot2017-07-26
|/ / / | | | | | | | | | | | | 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.
| * / Adding support for recursive notations of the form "x , .. , y , z".Gravatar Hugo Herbelin2017-07-26
|/ / | | | | | | | | | | | | | | | | 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.
* | Merge PR #899: [general] Move files to directories so they match linking order.Gravatar Maxime Dénès2017-07-20
|\ \
* \ \ Merge branch 'v8.7'Gravatar Maxime Dénès2017-07-20
|\ \ \
* \ \ \ Merge PR #770: [proof] Move bullets to their own module.Gravatar Maxime Dénès2017-07-19
|\ \ \ \
| | | * | [general] Move files to directories matching linking order.Gravatar Emilio Jesus Gallego Arias2017-07-19
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layersGravatar Maxime Dénès2017-07-17
|\ \ \ \
* \ \ \ \ Merge PR #862: Adding support for bindings tags to explicit prefix/suffix ↵Gravatar Maxime Dénès2017-07-17
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | rather than colors
| | * | | | Removing the uses of abstraction-breaking code in Lemmas.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I had to slightly tweak a test in order to work around a bug of simpl that loses universes constraints when refolding polymorphic fixpoints.
| | * | | | Removing the uses of abstraction-breaking code in Obligations.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | |
| | * | | | Remove the function Global.type_of_global_unsafe.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | |
| | * | | | The only abstraction-breaking function in Univ is now AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | |
| | * | | | Getting rid of AUContext abstraction breakers in Discharge.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | |
| | * | | | Make the typeclass implementation fully compatible with universe polymorphism.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This essentially means storing the abstract universe context in the typeclass data, and abstracting it when necessary.
| | * | | | Safer API for Global.body_of_constant and variants.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We aditionally return the abstract universe context inside the option. This is relatively painless as most uses were using the option as a boolean.
| | * | | | Safer API for Global.type_of_global_in_context.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | | | | | | | | | | | | | | | | | | | | We return the abstract context instead of an arbitrary instantiation.
| | * | | | Getting rid of AUContext abstraction breakers in Record.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | |
| | * | | | Getting rid of AUContext abstraction breakers in Search.Gravatar Pierre-Marie Pédrot2017-07-13
| |/ / / / |/| | | |
| | | * | Deprecate options that were introduced for compatibility with 8.5.Gravatar Théo Zimmermann2017-07-11
| | | | |
* | | | | Properly handling polymorphic inductive subtyping in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | | | | | | | | | | | | | | | | | | | | Before this patch, inductive subtyping was enforcing syntactic equality of the variable instance, instead of reasoning up to alpha-renaming.
* | | | | Safe API for accessing universe constraints of global references.Gravatar Pierre-Marie Pédrot2017-07-11
| |_|/ / |/| | | | | | | | | | | | | | | | | | | 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.
| * | | Adding support for bindings tags to explicit prefix/suffix rather than colors.Gravatar Hugo Herbelin2017-07-08
|/ / / | | | | | | | | | | | | | | | | | | | | | 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.
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
| | |
* | | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| | |
| | * Preparing to hints supporting discharge.Gravatar Hugo Herbelin2017-06-27
| |/ |/| | | | | | | I.e., do not set local flag to false when in a section since compatibility tells discharge of hints is not supported.
* | Merge PR#821: [vernac] Remove stale bool parameter from ↵Gravatar Maxime Dénès2017-06-23
|\ \ | | | | | | | | | `VernacStartTheoremProof`
| * | [vernac] Remove stale bool parameter from `VernacStartTheoremProof`Gravatar Emilio Jesus Gallego Arias2017-06-21
| | | | | | | | | | | | | | | `VernacStartTheoremProof` contained a stale bool parameter from 15 years ago, which is unused today.
* | | [vernac] Remove forward hooks from Obligations.Gravatar Emilio Jesus Gallego Arias2017-06-20
| | | | | | | | | | | | | | | | | | | | | This was (once again) a spurious inter-dependency, that we solve by introducing a new module with the proper functionality. This helps in cleaning up the code. Note that no code was changed, other than removing the setting of the references.
* | | [vernac] Remove unused hooks.Gravatar Emilio Jesus Gallego Arias2017-06-20
|/ / | | | | | | These hooks are not used (leftovers?) and IMHO they should not be.
* | Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
| |
* | Remove Warnings: unused value ...Gravatar Amin Timany2017-06-16
| |
* | Change the option to Set Inductive CumulativityGravatar Amin Timany2017-06-16
| | | | | | | | | | This requires to change the status of Inductive (we have also changed CoInductive and Variant) from keyword to identifier.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 22:12:38 +0000