aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/vernacexpr.mli
Commit message (Collapse)AuthorAge
* Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
|
* Merge PR#417: No cast surgery in let inGravatar Maxime Dénès2017-04-03
|\
* | [stm] Remove some obsolete vernacs/classification.Gravatar Emilio Jesus Gallego Arias2017-03-24
| | | | | | | | | | | | | | | | | | | | This is the good parts of PR #360. IIUC, these vernacular were meant mostly for debugging and they are not supposed to be of any use these days. Back and join are still there not to break the testing infrastructure, but some day they should go away.
| * Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
|/ | | | This is a bit long, but it is to keep a symmetry with constr_expr.
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\
| * Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Gravatar Maxime Dénès2016-11-18
| | | | | | | | | | | | | | | | | | This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341. It turns out that calling from fake_ide the STM commands that were removed by this PR requires an extension of the XML protocol. So postponing the integration.
| * [stm] Remove STM-related vernacularsGravatar Emilio Jesus Gallego Arias2016-11-17
| | | | | | | | | | | | | | | | | | I think these commands never make a lot of sense on scripts other than debugging and we have better methods now. The last remaining command, used for the tty emulation has been renamed to VtBack, but it should go away at some point too once the legacy interfaces are removed.
| * Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
| | | | | | | | | | | | | | | | | | In addition to a priority, cleanup the interfaces for passing this information as well. The pattern, if given, takes priority over the inferred one. We only allow Existing Instances gr ... gr | pri. for now, without pattern, as before. Make the API compatible to 8.5 as well.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\|
| * Complete overhaul of the Arguments vernacular.Gravatar Maxime Dénès2016-10-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The main point of this change is to fix #3035: Avoiding trailing arguments in the Arguments command, and related issues occurring in HoTT for instance. When the "assert" flag is not specified, we now accept prefixes of the list of arguments. The semantics of _ w.r.t. to renaming has changed. Previously, it meant "restore the original name inferred from the type". Now it means "don't change the current name". The syntax of arguments is now restricted. Modifiers like /, ! and scopes are allowed only in the first arguments list. We also add *a lot* of missing checks on input values and fix various bugs. Note that this code is still way too complex for what it does, due to the complexity of the implicit arguments, reduction behaviors and renaming APIs.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\|
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\ \
| | * Add command 'Set foo Append "bar"' for appending to an option (bug #5109).Gravatar Guillaume Melquiond2016-10-01
| |/ | | | | | | | | | | | | | | | | | | For now, the only meaningful user is "Set Warnings". Example: Section Bar. Local Set Warnings Append "-foo". (* warning foo is now disabled *) End Bar. (* foo is now reenabled, assuming it was before entering the section *)
| * Merge remote-tracking branch 'github/pr/299' into v8.6Gravatar Maxime Dénès2016-09-30
| |\ | | | | | | | | | | | | Was PR#299: Fix bug #4869, allow Prop, Set, and level names in constraints.
| * | Fix bug #4798: compat notations should not modify the parser.Gravatar Pierre-Marie Pédrot2016-09-29
| | | | | | | | | | | | | | | | | | This is a quick fix. The Metasyntax module should be thoroughly revised in trunk, because it starts featuring a lot of spaghetti code and redundant data.
| * | Arguments: cleanup + detect discrepancy rename/implicit (#3753)Gravatar Enrico Tassi2016-09-29
| | | | | | | | | | | | | | | It seems warnings are not taken into account in output/ tests.
| | * Fix bug #4869, allow Prop, Set, and level names in constraints.Gravatar Matthieu Sozeau2016-09-29
| |/
* / Making Vernacexpr independent from Tacexpr.Gravatar Pierre-Marie Pédrot2016-09-08
|/
* Support qualified identifiers in Show Match (bug #5050).Gravatar Guillaume Melquiond2016-08-27
|
* COMMENTS: Vernacexpr.extend_nameGravatar Matej Kosik2016-06-20
|
* par: like all: but in parallelGravatar Enrico Tassi2016-06-17
| | | | | | | | | | | | | This commit documents par:, fixes its semantics so that is behaves like all:, supports (toplevel) abstract and optimizes toplevel solve. `par: solve [tac]` is equivalent to `Ltac tac1 := solve[tac]...par: tac1` but is optimized for failures: if one goal fails all are aborted immediately. `par: abstract tac` runs abstract on the generated proof terms. Nested abstract calls are not supported.
* Extend Hint Mode to handle the no-head-evar caseGravatar Matthieu Sozeau2016-06-16
| | | | | | | Suggested by R. Krebbers and C. Cohen, this makes modes more applicable, by allowing to trigger resolution on partially instantiated indices. This is a rough but fast approximation of the pattern on which one would like instances to apply.
* Merge 'pr/191' into trunkGravatar Enrico Tassi2016-06-16
|\
* \ Merge remote-tracking branch 'github/pr/194' into trunkGravatar Maxime Dénès2016-06-16
|\ \
| | * Goal selectors are now tacticals and can be used as such.Gravatar Cyprien Mangin2016-06-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows to write things like this: split; 2: intro _; exact I or like this: eexists ?[x]; ?[x]: exact 0; trivial This has the side-effect on making the '?' before '[x]' mandatory.
| | * Add goal range selectors.Gravatar Cyprien Mangin2016-06-14
| | | | | | | | | | | | | | | You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals numbered 1 and 3 to 5.
| * | Adding an only printing flag to notations.Gravatar Pierre-Marie Pédrot2016-06-07
| |/
* / STM: proof block detection/error resilience APIGravatar Enrico Tassi2016-06-06
|/ | | | | | | | | | | | This commit introduces the concept of proof blocks that are resilient to errors. They are represented as ErrorBound boxes in the STM document with the topological invariant that they never overlap. The detection and error recovery of ErrorBound boxes is defined outside the STM. One can define a box by providing a function to detect it statically by crawling the parsed document and a function to recover from an error at run time.
* Moving and enhancing the grammar_tactic_prod_item_expr type.Gravatar Pierre-Marie Pédrot2016-04-14
|
* Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵Gravatar Matthieu Sozeau2016-04-04
|\ | | | | | | into JasonGross-trunk-function_scope
* | Moving the Ltac definition command to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
| |
* | Moving Print Ltac to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
| |
* | Moving Tactic Notation to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
| |
* | Moving VernacSolve to an EXTEND-based definition.Gravatar Pierre-Marie Pédrot2016-03-19
| |
* | Moving Autorewrite to Hightatctic.Gravatar Pierre-Marie Pédrot2016-03-06
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\ \
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
| | |
* | | CLEANUP: removing unnecessary wrapperGravatar Matej Kosik2016-01-11
| | |
* | | Simplification of grammar_prod_item type.Gravatar Pierre-Marie Pédrot2016-01-02
| | | | | | | | | | | | Actually the identifier was never used and just carried along.
* | | CLEANUP: removing unnecessary aliasGravatar Matej Kosik2015-12-18
| | |
* | | CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionGravatar Matej Kosik2015-12-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The definition of Vernacexpr.VernacDeclareTacticDefinition was changed. The original definition allowed us to represent non-sensical value such as: VernacDeclareTacticDefinition(Qualid ..., false, ...) The new definition prevents that.
* | | CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular ↵Gravatar Matej Kosik2015-12-18
| | | | | | | | | | | | command is mapped.
* | | CLEANUP: Vernacexpr.vernac_exprGravatar Matej Kosik2015-12-18
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Originally, "VernacTime" and "VernacRedirect" were defined like this: type vernac_expr = ... | VernacTime of vernac_list | VernacRedirect of string * vernac_list ... where type vernac_list = located_vernac_expr list Currently, that list always contained one and only one element. So I propose changing the definition of these two variants in the following way: | VernacTime of located_vernac_expr | VernacRedirect of string * located_vernac_expr which covers all our current needs and enforces the invariant related to the number of commands that are part of the "VernacTime" and "VernacRedirect" variants.
* | Adding syntax "Show id" to show goal named id (shelved or not).Gravatar Hugo Herbelin2015-11-02
| |
* | Axioms now support the universe binding syntax.Gravatar Pierre-Marie Pédrot2015-10-08
| | | | | | | | | | | | We artificially restrict the syntax though, because it is unclear of what the semantics of several axioms in a row is, in particular about the resolution of remaining evars.
* | Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
| | | | | | | | | | | | | | | | | | | | | | | | | | - "Proof using p*" means: use p and any section var about p. - Simplify the grammar/parser for proof using <expression>. - Section variables with a body (let-in) are pulled in automatically since they are safe to be used (add no extra quantification) - automatic clear of "unused" section variables made optional: Set Proof Using Clear Unused. since clearing section hypotheses does not "always work" (e.g. hint databases are not really cleaned) - term_typing: trigger a "suggest proof using" message also for Let theorems.
* | Goptions: new value type: optional stringGravatar Enrico Tassi2015-10-08
| | | | | | | | | | These options can be set to a string value, but also unset. Internal data is of type string option.
* | Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
| | | | | | | | | | ... lemmas and inductives to control which universes are bound and where in universe polymorphic definitions. Names stay outside the kernel.
* | Documentation by giving a name to a large type.Gravatar Pierre-Marie Pédrot2015-08-19
| |
| * Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Gravatar Jason Gross2015-08-14
|/ | | | | | | | | | | | | | | | | | | | | | | This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change in the semantics of arguments scopes: scopes can no longer be bound to Funclass or Sortclass (this does not seem to be useful)). It is useful to have function_scope for, e.g., function composition. This allows users to, e.g., automatically interpret ∘ as morphism composition when expecting a morphism of categories, as functor composition when expecting a functor, and as function composition when expecting a function. Additionally, it is nicer to have fewer special cases in the OCaml code, and give more things a uniform syntax. (The scope type_scope should not be special-cased; this change is coming up next.) Also explicitly define [function_scope] in theories/Init/Notations.v. This closes bug #3080, Build a [function_scope] like [type_scope], or allow [Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass] We now mention Funclass and Sortclass in the documentation of [Bind Scope] again.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 03:05:31 +0000