aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Collapse)AuthorAge
...
* 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.
* Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | The motivations are: - To reflect the concrete syntax more closely. - To factorize the different places where "contexts" are internalized: before this patch, there is a different treatment of `Definition f '(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack to interpret `Definition f `pat := c : t`. With the patch, the fix to avoid seeing a variable named `pat` works for both `fun 'x => ...` and `Definition f 'x := ...`. The drawbacks are: - Counterpart to reflecting the concrete syntax more closerly, there are more redundancies in the syntax. For instance, the case `CLetIn (na,b,t,c)` can appears also in the form `CProdN (CLocalDef (na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`. - Changes in the API, hence adaptation of plugins referring to `constr_expr` needed.
* Merge PR #1082: Fixing Print for inductive types with let-in in parametersGravatar Maxime Dénès2018-02-12
|\
* \ Merge PR #6128: Simplification: cumulativity information is variance ↵Gravatar Maxime Dénès2018-02-12
|\ \ | | | | | | | | | information.
* \ \ Merge PR #6651: Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-02-12
|\ \ \
| | * | Print inductive cumulativity info in About.Gravatar Gaëtan Gilbert2018-02-11
| | | |
| | * | Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since cumulativity of an inductive type is the universe constraints which make a term convertible with its universe-renamed copy, the only constraints we can get are between a universe and its copy. As such we do not need to be able to represent arbitrary constraints between universes and copied universes in a double-sized ucontext, instead we can just keep around an array describing whether a bound universe is covariant, invariant or irrelevant (CIC has no contravariant conversion rule). Printing is fairly obtuse and should be improved: when we print the CumulativityInfo we add marks to the universes of the instance: = for invariant, + for covariant and * for irrelevant. ie Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }. Print Foo. gives Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo { foo : Type@{i} -> Type@{j} } (* =i +j *k |= *)
* | | [vernac] Mutual theorems (VernacStartTheoremProof) always have namesGravatar Vincent Laporte2018-02-01
| | |
* | | [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionGravatar Vincent Laporte2018-02-01
| | |
| * | Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-01-30
|/ / | | | | | | | | | | | | | | | | | | | | | | | | There is no way today to distinguish primitive projections from compatibility constants, at least in the case of a record without parameters. We remedy to this by always using the r.(p) syntax when printing primitive projections, even with Set Printing All. The input syntax r.(p) is still elaborated to GApp, so that we can preserve the compatibility layer. Hopefully we can make up a plan to get rid of that layer, but it will require fixing a few problems.
* | [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.
* | Merge PR #6433: [flags] Move global time flag into an attribute.Gravatar Maxime Dénès2017-12-29
|\ \
* | | [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
| | | | | | | | | | | | | | | | | | | | | | | | Unfortunately OCaml doesn't deprecate the constructors of a type when the type alias is deprecated. In this case it means that we don't get rid of the kernel dependency unless we deprecate the constructors too.
| * | [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.
* | Merge PR #978: In printing, experimenting factorizing "match" clauses with ↵Gravatar Maxime Dénès2017-12-14
|\ \ | | | | | | | | | same right-hand side.
| | * Fixing a bug of Print for inductive types with let-ins in parameters.Gravatar Hugo Herbelin2017-12-14
| | | | | | | | | | | | | | | | | | | | | Adding a "let-in"-sensitive function hnf_prod_applist_assum to instantiate parameters and using it for printing. Thanks to PMP for reporting.
| * | Removing cumbersome location in multiple patterns.Gravatar Hugo Herbelin2017-12-12
| | | | | | | | | | | | This is to have a better symmetry between CCases and GCases.
| * | Improving spacing in printing disjunctive patterns.Gravatar Hugo Herbelin2017-12-12
| |/ | | | | | | | | Adding a space before the bar separating disjunctive patterns. Removing an extra space after the bar for inner disjunctive patterns.
* / [proof] Embed evar_map in RefinerError exception.Gravatar Emilio Jesus Gallego Arias2017-12-11
|/ | | | | | | | | The exception needs to carry aroud a pair of `env, sigma` so printing is correct. This gets rid of a few global calls, and it is IMO the right thing to do. While we are at it, we incorporate some fixes to a couple of additional printing functions missing the `env, sigma` pair.
* Merge PR #6158: Allows a level in the raw and glob printersGravatar Maxime Dénès2017-12-08
|\
* | Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
| | | | | | | | | | | | | | | | They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced
* | Merge PR #6233: [proof] [api] Rename proof types in preparation for ↵Gravatar Maxime Dénès2017-12-01
|\ \ | | | | | | | | | functionalization.
* \ \ Merge PR #1049: Remove obsolete localityGravatar Maxime Dénès2017-11-30
|\ \ \
* \ \ \ Merge PR #6244: [lib] [api] Introduce record for `object_prefix`Gravatar Maxime Dénès2017-11-30
|\ \ \ \
| | * | | 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.
| * | | [lib] [api] Introduce record for `object_prefix`Gravatar Emilio Jesus Gallego Arias2017-11-29
| | | | | | | | | | | | | | | | | | | | This is a minor cleanup adding a record in a try to structure the state living in `Lib`.
| | * | [proof] [api] Rename proof types in preparation for functionalization.Gravatar Emilio Jesus Gallego Arias2017-11-29
| |/ / |/| | | | | | | | | | | In particular `Proof_global.t` will become a first class object for the upper parts of the system in a next commit.
* | | Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\ \ \
* | | | [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
| |/ / |/| | | | | | | | | | | There don't really bring anything, we also correct some minor nits with the printing function.
| * | Allow local universe renaming in Print.Gravatar Gaëtan Gilbert2017-11-25
| | |
| * | When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | | | | | | | | | | | | | Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved.
| * | Separate checking univ_decls and obtaining universe binder names.Gravatar Gaëtan Gilbert2017-11-24
|/ /
| * Extending further PR#6047 (system to register printers for Ltac values).Gravatar Hugo Herbelin2017-11-24
|/ | | | | | | We generalize the possible use of levels to raw and glob printers. This is potentially useful for printing ltac expressions which are the glob level.
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
| | | | | | | We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`.
* [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.
* [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
| | | | | | | | | | | We'd like to handle proofs functionally we thus recommend not to use printing functions without an explicit context. We also adapt most of the code, making more explicit where the printing environment is coming from. An open task is to refactor some code so we gradually make the `Pfedit.get_current_context ()` disappear.
* Merge PR #6185: [parser] Remove unnecessary statically initialized hook.Gravatar Maxime Dénès2017-11-21
|\
| * [parser] Remove unnecessary statically initialized hook.Gravatar Emilio Jesus Gallego Arias2017-11-19
| | | | | | | | | | | | | | | | | | | | | | | | | | Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to put any pattern in binders, prefixed by a quote."] its current placement as well as the hook don't make a lot of sense. In particular, they prevent parts of Coq working without linking the parser. To this purpose, we need to consolidate the `Constrexpr` utilities. While we are at it we do so and remove the `Topconstr` module which is fully redundant with `Constrexpr_ops`.
* | [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Emilio Jesus Gallego Arias2017-11-19
|/ | | | | | | | | | | | I followed what seems to be the intention of the code, with the original intention of remove the global imperative proof state. However, I fully fail to see why the new API is better than the old one. In fact the opposite seems the contrary. Still big parts of the "new proof engine" seem unfinished, and I'm afraid I am not the right person to know what direction things should take.
* [api] Insert miscellaneous API deprecation back to core.Gravatar Emilio Jesus Gallego Arias2017-11-13
|
* [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
|
* Merge PR #6098: [api] Move structures deprecated in the API to the core.Gravatar Maxime Dénès2017-11-13
|\