aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Collapse)AuthorAge
...
* | Merge PR #6103: Hack to restore printing of glob_constr in debugger.Gravatar Maxime Dénès2017-11-13
|\ \
| * | Hack to restore printing of glob_constr in debugger.Gravatar Hugo Herbelin2017-11-07
| | |
| | * [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| |/ |/| | | | | We do up to `Term` which is the main bulk of the changes.
* | [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
|/ | | | This will allow to merge back `Names` with `API.Names`
* Finish removing Show Goal uidGravatar Gaëtan Gilbert2017-11-04
| | | | Syntax removed in faa064c746e20a12b3c8f792f69537b18e387be6
* Setting a system to register printers for Ltac values.Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | | | | | | | The model provides three kinds of printers depending on whether the printer needs a context, and, if yes if it supports levels. In the latter case, it takes defaults levels for printing when in a surrounded context (lconstr style) and for printing when not in a surrounded context (constr style). This model preserves the 8.7 focussing semantics of "idtac" (i.e. focussing only when an env is needed) but it also shows that the semantics of "idtac", which focusses the goal depending on the type of its arguments, is a bit ad hoc to understand. See discussion at PR#6047 "https://github.com/coq/coq/pull/6047#discussion_r148278454".
* Using a specific function to register vernac printers.Gravatar Hugo Herbelin2017-11-02
|
* Exporting the level-parametric printer of constr and its variants.Gravatar Hugo Herbelin2017-11-02
| | | | This is for eventually being reused in Ltac messages ("idtac").
* Removing a redundancy in naming types (Ppconstr.precedence = tolerability).Gravatar Hugo Herbelin2017-11-02
|
* Merge PR #6015: [general] Remove Econstr dependency from `intf`Gravatar Maxime Dénès2017-10-27
|\
| * [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
| | | | | | | | | | To this extent we factor out the relevant bits to a new file, ltac_pretype.
* | An occurrence of set_id which behaves as the identity.Gravatar Hugo Herbelin2017-10-24
|/
* Parse [Proof using Type] without translating Type to an id.Gravatar Gaëtan Gilbert2017-10-10
|
* [vernac] Remove "Proof using" hacks from parser.Gravatar Emilio Jesus Gallego Arias2017-10-10
| | | | | | | | | We place `Proof_using` in the proper place [`vernac`] and we remove gross parsing hacks. The new placement should allow to use the printers and more convenient structure, and reduce strange coupling between parsing and internal representation.
* Implementing a generic mechanism for locating named objects from Coq side.Gravatar Pierre-Marie Pédrot2017-10-03
|
* Moving the Ltac-specific part of the nametab to the Ltac plugin.Gravatar Pierre-Marie Pédrot2017-10-03
| | | | | For now, a few vernacular features were lot in the process, like locating Ltac definitions. This will be fixed in an upcoming commit.
* Merge PR #1040: Efficient fresh name generationGravatar Maxime Dénès2017-10-03
|\
* | [vernac] Remove `Qed exporting` syntax.Gravatar Emilio Jesus Gallego Arias2017-09-29
| | | | | | | | | | | | | | We don't gain anything from the kernel yet as transparent constants _do_ require the `side_eff` exporting machinery. Next step, understand why.
| * Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
|/ | | | | The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n).
* Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\
* \ Merge PR #1057: Reporting locations in error messages about notation formats.Gravatar Maxime Dénès2017-09-25
|\ \
* | | Remove STM vernaculars.Gravatar Maxime Dénès2017-09-19
| | |
| | * Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | Introduce a "+" modifier for universe and constraint declarations to indicate that these can be extended in the final definition/proof. By default [Definition f] is equivalent to [Definition f@{+|+}], i.e universes can be introduced and constraints as well. For [f@{}] or [f@{i j}], the constraints can be extended, no universe introduced, to maintain compatibility with existing developments. Use [f@{i j | }] to indicate that no constraint (nor universe) can be introduced. These kind of definitions could benefit from asynchronous processing. Declarations of universe binders and constraints also works for monomorphic definitions.
| * Reporting locations in error messages about notation formats.Gravatar Hugo Herbelin2017-09-18
|/
* Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵Gravatar Maxime Dénès2017-09-15
|\ | | | | | | top of the linking chain.
* \ Merge PR #1037: Parse directly to Sorts.family when appropriate.Gravatar Maxime Dénès2017-09-15
|\ \
* | | Don't exclude a priori CLocalDef to be treated by ppconstr.ml.Gravatar Hugo Herbelin2017-09-12
| | |
| * | Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
|/ / | | | | | | | | When we used to parse to a glob_sort but always give an empty list in the GType case we can now parse directly to Sorts.family.
| * [vernac] Store Infix Modifier in Vernac Notation.Gravatar Pierre-Marie Pédrot2017-08-29
|/ | | | This removes a dependency from `G_vernac` to `Metasyntax`.
* Merge PR #916: Fixing notation bug 5608 involving { } and a slight ↵Gravatar Maxime Dénès2017-08-29
|\ | | | | | | restructuration
* \ Merge PR #830: Moving assert (the "Cut" rule) to new proof engineGravatar Maxime Dénès2017-08-29
|\ \
| | * A new step of restructuration of notations.Gravatar Hugo Herbelin2017-08-29
| |/ |/| | | | | | | | | | | 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).
* | Merge PR #912: Detyping functions are now operating on EConstr.t.Gravatar Maxime Dénès2017-08-16
|\ \
* \ \ Merge PR #864: Some cleanups after cumulativity for inductive typesGravatar Maxime Dénès2017-08-16
|\ \ \
| | * | Printing goals does not evar-normalizes beforehand anymore.Gravatar Pierre-Marie Pédrot2017-08-01
| | | |
| | * | 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
|\ \ \
| | * | 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.
* | | | 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.
* | Merge PR #899: [general] Move files to directories so they match linking order.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.
* | | 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
| | |
* | | Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Gravatar Pierre-Marie Pédrot2017-07-13
| | |
* | | 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.
* | | Moving the last bits of abtraction-breaking code out of the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 01:04:23 +0000