aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppvernac.ml
Commit message (Collapse)AuthorAge
* [api] Move `opacity_flag` to `Proof_global`.Gravatar Emilio Jesus Gallego Arias2018-05-23
| | | | | | | `Proof_global` is the main consumer of the flag, which doesn't seem to belong to the AST as plugins show. This will allow the vernac AST to be placed in `vernac` indeed.
* Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.Gravatar Pierre-Marie Pédrot2018-05-04
|\
* | [api] Move bullets and goals selectors to `proofs/`Gravatar Emilio Jesus Gallego Arias2018-05-01
| | | | | | | | | | | | | | | | | | | | `Vernacexpr` lives conceptually higher than `proof`, however, datatypes for bullets and goal selectors are in `Vernacexpr`. In particular, we move: - `proof_bullet`: to `Proof_bullet` - `goal_selector`: to a new file `Goal_select`
| * [api] Move `hint_info_expr` to `Typeclasses`.Gravatar Emilio Jesus Gallego Arias2018-04-26
|/ | | | | | `hint_info_expr`, `hint_info_gen` do conceptually belong to the typeclasses modules and should be able to be used without a dependency on the concrete vernacular syntax.
* [api] Remove dependency of library on Vernacexpr.Gravatar Emilio Jesus Gallego Arias2018-04-06
| | | | | | | | | Morally, `library` should not depend on the vernacular definition. This will also create problems when trying to modularize the codebase due to the cycle [vernacs depend for example on constrexprs]. The fix is fortunately easy.
* Merge PR #7016: Make parsing independent of the cumulativity flag.Gravatar Enrico Tassi2018-04-05
|\
* \ Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.Gravatar Enrico Tassi2018-04-04
|\ \
| * | [stm] Move VernacBacktrack to the toplevel.Gravatar Emilio Jesus Gallego Arias2018-04-01
| | | | | | | | | | | | | | | | | | This command is legacy, equivalent to `EditAt` and only used by Emacs. We move it to the toplevel so we can kill some legacy code and in particular the `part_of_script` hack.
* | | Remove deprecated commands Arguments Scope and Implicit ArgumentsGravatar Jasper Hugunin2018-03-30
|/ /
| * bool option -> (VernacCumulative | VernacNonCumulative) optionGravatar Gaëtan Gilbert2018-03-22
| |
| * Make parsing independent of the cumulativity flag.Gravatar Gaëtan Gilbert2018-03-21
| |
* | [vernac] Move `Quit` and `Drop` to the toplevel layer.Gravatar Emilio Jesus Gallego Arias2018-03-11
|/ | | | | | This is a first step towards moving REPL-specific commands out of the core layers. In particular, we remove `Quit` and `Drop` from the core vernacular to specific toplevel-level parsing rules.
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
| | | | | | | | | | | We continue with the work of #402 and #6745 and update most of the remaining parts of the AST: - module declarations - intro patterns - top-level sentences Now, parsed documents should be full annotated by `CAst` nodes.
* Implement the Export Set/Unset feature.Gravatar Pierre-Marie Pédrot2018-03-09
| | | | | | | This feature has been asked many times by different people, and allows to have options in a module that are performed when this module is imported. This supersedes the well-numbered cursed PR #313.
* Merge PR #6790: Allow universe declarations for [with Definition].Gravatar Maxime Dénès2018-03-07
|\
| * Allow universe declarations for [with Definition].Gravatar Gaëtan Gilbert2018-03-05
| |
* | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
| | | | | | | | | We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
* Change default for notations with variables bound to both terms and binders.Gravatar Hugo Herbelin2018-02-20
| | | | For compatibility, the default is to parse as ident and not as pattern.
* Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | Concretely, we provide "constr as ident", "constr as strict pattern" and "constr as pattern". This tells to parse a binder as a constr, restricting to only ident or to only a strict pattern, or to a pattern which can also be an ident. The "strict pattern" modifier allows to restrict the use of patterns in printing rules. This allows e.g. to select the appropriate rule for printing between {x|P} and {'pat|P}.
* Notations: A step in cleaning constr_entry_key.Gravatar Hugo Herbelin2018-02-20
| | | | | | - Avoid dummy use of unit - Do not decide as early as parsing the default level for pattern - Prepare to further extensions
* Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | This allows in particular to define notations with 'pat style binders. E.g.: A non-trivial change in this commit is storing binders and patterns separately from terms. This is not strictly necessary but has some advantages. However, it is relatively common to have binders also used as terms, or binders parsed as terms. Thus, it is already relatively common to embed binders into terms (see e.g. notation for ETA in output test Notations3.v) or to coerce terms to idents (see e.g. the notation for {x|P} where x is parsed as a constr). So, it is as simple to always store idents (and eventually patterns) as terms.
* Introducing an intermediary type "constr_prod_entry_key" for grammar ↵Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | productions. This type describes the grammar non-terminal. It typically contains ETConstrList (now renamed ETProdConstrList) but not ETBinder. It is the type for metasyntax.ml and egramcoq.ml to communicate together. The type constr_prod_entry_key with ETConstr, ETBinder, is now used only in metasyntax.ml. This allows to get rid of some "assert false" in uselessly matching over ETConstrList in metasyntax.ml and of some "assert false" in uselessly matching over ETBinder in egramcoq.ml. Also exporting less of extend.mli in API.
* [vernac] Mutual theorems (VernacStartTheoremProof) always have namesGravatar Vincent Laporte2018-02-01
|
* [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionGravatar Vincent Laporte2018-02-01
|
* [printing] Remove duplicate definitions of pr_lident and pr_lnameGravatar Vincent Laporte2018-01-22
|
* Merge PR #6499: [vernac] Move the flags/attributes out of vernac_exprGravatar Maxime Dénès2018-01-16
|\
| * [vernac] vernac_expr no longer recursiveGravatar Vincent Laporte2018-01-08
| |
* | Brackets support single numbered goal selectors.Gravatar Théo Zimmermann2018-01-05
|/ | | | | This allows to focus on a sub-goal other than the first one without resorting to the `Focus` command.
* [flags] Move global time flag into an attribute.Gravatar Emilio Jesus Gallego Arias2017-12-23
| | | | One less global flag.
* Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
| | | | | | | | | | | | Virtually all classifications of vernacular commands (the STM classifier, "filtered commands", "navigation commands", etc.) were broken in presence of control vernaculars like Time, Timeout, Fail. Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac Debug in CoqIDE. This change introduces a type separation between vernacular controls and vernacular commands, together with an "under_control" combinator.
* Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
| | | | | | | | | | We remove deprecated syntax "Coercion Local" and such, and seize the opportunity to refactor some code around vernac_expr. We also do a small fix on the STM classification, which didn't know about Let Fixpoint and Let CoFixpoint. This is a preliminary step for the work on attributes.
* Allow local universe renaming in Print.Gravatar Gaëtan Gilbert2017-11-25
|
* [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
| | | | | | We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization.
* Finish removing Show Goal uidGravatar Gaëtan Gilbert2017-11-04
| | | | Syntax removed in faa064c746e20a12b3c8f792f69537b18e387be6
* 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
|
* [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.
* Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\
* | 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.
* Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵Gravatar Maxime Dénès2017-09-15
|\ | | | | | | top of the linking chain.
* | 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`.
* 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 #770: [proof] Move bullets to their own module.Gravatar Maxime Dénès2017-07-19
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| |
* | [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.
* | Add printing of cumulativity in inductive typesGravatar Amin Timany2017-06-16
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 07:29:30 +0000