aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
Commit message (Collapse)AuthorAge
* Make most of TACTIC EXTEND macros runtime calls.Gravatar Maxime Dénès2018-03-08
| | | | | | | | | Today, TACTIC EXTEND generates ad-hoc ML code that registers the tactic and its parsing rule. Instead, we make it generate a typed AST that is passed to the parser and a generic tactic execution routine. PMP has written a small parser that can generate the same typed ASTs without relying on camlp5, which is overkill for such simple macros.
* Merge PR #6905: Fix make ml-docGravatar Maxime Dénès2018-03-07
|\
* \ Merge PR #6790: Allow universe declarations for [with Definition].Gravatar Maxime Dénès2018-03-07
|\ \
| | * Change non-documentation comment from ocamldoc styleGravatar mrmr19932018-03-05
| | |
| | * Fix formatting of some ocamldoc comments to reduce warningsGravatar mrmr19932018-03-05
| |/ |/|
| * 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 general support for irrefutable disjunctive patterns.Gravatar Hugo Herbelin2018-02-20
| | | | | This now works not only for parsing of fun/forall (as in 8.6), but also for arbitraty notations with binders and for printing.
* Respecting the ident/pattern distinction in notation modifiers.Gravatar Hugo Herbelin2018-02-20
|
* 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.
* Allows recursive patterns for binders to be associative on the left.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | This makes treatment of recursive binders closer to the one of recursive terms. It is unclear whether there are interesting notations liable to use this, but this shall make easier mixing recursive binders and recursive terms as in next commits. Example of (artificial) notation that this commit supports: Notation "! x .. y # A #" := (.. (A,(forall x, True)) ..,(forall y, True)) (at level 200, x binder).
* A bit of miscellaneous code documentation around notations.Gravatar Hugo Herbelin2018-02-20
|
* 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.
* Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.Gravatar Hugo Herbelin2018-02-20
|
* More precise explanation when a notation is not reversible for printing.Gravatar Hugo Herbelin2018-02-20
|
* Merge PR #6651: Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-02-12
|\
* | [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.
* 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.
| * [vernac] Define types in orderGravatar Vincent Laporte2017-12-29
|/
* 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.
| * In printing, factorizing "match" clauses with same right-hand side.Gravatar Hugo Herbelin2017-12-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Moreover, when there are at least two clauses and the last most factorizable one is a disjunction with no variables, turn it into a catch-all clause. Adding options Unset Printing Allow Default Clause. to deactivate the second behavior, and Unset Printing Factorizable Match Patterns. to deactivate the first behavior (deactivating the first one deactivates also the second one). E.g. printing match x with Eq => 1 | _ => 0 end gives match x with | Eq => 1 | _ => 0 end or (with default clause deactivates): match x with | Eq => 1 | Lt | Gt => 0 end More to be done, e.g. reconstructing multiple patterns in Nat.eqb...
| * Removing cumbersome location in multiple patterns.Gravatar Hugo Herbelin2017-12-12
| | | | | | | | This is to have a better symmetry between CCases and GCases.
* | Merge PR #1150: [stm] Remove all but one use of VtUnknown.Gravatar Maxime Dénès2017-12-11
|\ \
* | | [api] Remove kernel dependency on intf (Decl_kind)Gravatar Emilio Jesus Gallego Arias2017-12-10
| |/ |/| | | | | | | | | We more the `recursivity_kind` type to `Declarations`, this indeed makes sense, and now `Decl_kind` morally lives in `library` as it should.
| * [stm] Remove all but one use of VtUnknown.Gravatar Emilio Jesus Gallego Arias2017-12-09
|/ | | | | | | | | Together with #1122, this makes `VernacInstance` the only command in the Coq codebase that cannot be statically determined to open a proof. The reasoning for the commands moved to `VtSideff` is that parser-altering commands should be always marked `VtNow`; the rest can be usually marked as `VtLater`.
* 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
* 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.
* 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
|/
* Merge PR #6098: [api] Move structures deprecated in the API to the core.Gravatar Maxime Dénès2017-11-13
|\
* \ Merge PR #6052: [general] Move Tactypes to `interp` + API reordering.Gravatar Maxime Dénès2017-11-13
|\ \
| | * [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.
* | Finish removing Show Goal uidGravatar Gaëtan Gilbert2017-11-04
| | | | | | | | Syntax removed in faa064c746e20a12b3c8f792f69537b18e387be6
| * [general] Move Tactypes to `interp`Gravatar Emilio Jesus Gallego Arias2017-11-01
|/ | | | | | This makes sense here as the main client is `Stdargs`. This helps with the concerns @herbelin had in https://github.com/coq/coq/issues/6008#issuecomment-341107793
* [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.
* [stm] Remove VtBack from public classification.Gravatar Emilio Jesus Gallego Arias2017-10-17
| | | | | | | | | We interpret meta-commands directly, instead of going by an intermediate "classifier step". The code could still use some further refactoring, in particular, the `part_of_script` bit is a bit strange likely coming from some special treatment of `VtMeta` in the `query` call, and should go away.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 09:29:33 +0000