aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_vernac.ml4
Commit message (Collapse)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\
| * Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
| |
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
| |
* | 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 the parsing of the Ltac proof mode to G_ltac.Gravatar Pierre-Marie Pédrot2016-03-19
| | |
* | | Moving the proof mode parsing management to Pcoq.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-29
|\ \ \ | | |/ | |/|
| * | Implement support for universe binder lists in Instance and Program ↵Gravatar Matthieu Sozeau2016-01-23
| | | | | | | | | | | | Fixpoint/Definition.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\| |
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
| | |
* | | Simplification of grammar_prod_item type.Gravatar Pierre-Marie Pédrot2016-01-02
| | | | | | | | | | | | Actually the identifier was never used and just carried along.
* | | ALPHA-CONVERSION: in "parsing/g_vernac.ml4" fileGravatar Matej Kosik2015-12-18
| | |
* | | 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.
* | Allowing empty bound universe variables.Gravatar Pierre-Marie Pédrot2015-10-08
| |
* | 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.
* | Record fields accept an optional final semicolon separator.Gravatar Pierre-Marie Pédrot2015-10-07
| | | | | | | | | | There is no such thing as the OPTSEP macro in Camlp4 so I had to expand it by hand.
* | 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.
* | Hacking parser so as to support both [> ... ] and [id].Gravatar Hugo Herbelin2015-09-08
| | | | | | | | This (at least technically) solves the issue #4113 (see also #4329).
| * 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.
* Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Gravatar Lionel Rieg2015-06-26
|
* Granting, undocumentedly, parsing of "Conjectures" as a synonym ofGravatar Hugo Herbelin2015-06-16
| | | | "Conjecture" (see #4252).
* Add a [Redirect] vernacular commandGravatar Clément Pit--Claudel2015-05-04
| | | | | | | The command [Redirect "filename" (...)] redirects all the output of [(...)] to file "filename.out". This is useful for storing the results of an [Eval compute], for redirecting the results of a large search, for automatically generating traces of interesting developments, and so on.
* Putting the From parameter of the Require command into the AST.Gravatar Pierre-Marie Pédrot2015-03-27
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Better doc and a few fixes for Proof using.Gravatar Enrico Tassi2014-12-19
|
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
|
* About now accepts hypothesis names and goal selector.Gravatar Pierre Courtieu2014-12-15
|
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
| | | | Documentation also updated.
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
|
* Add [Info] command.Gravatar Arnaud Spiwack2014-11-01
| | | | Called with [Info n tac], runs [tac] and prints its info trace unfolding [n] level of tactic names ([0] for no unfolding at all).
* Emit a warning for void Arguments statement (Close 3713)Gravatar Enrico Tassi2014-10-13
|
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
| | | | | | | | will name the goal id; writing ?[?id] will use the first fresh name available based with prefix id. Tactics intro, rename, change, ... from logic.ml now preserve goal name; cut preserves goal name on its main premise.
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
| | | | | | | | | | | so that one can retrieve them and pass them to third party tools (i.e. print the AST with the notations attached to the nodes concerned). Available syntax: - all in one: Notation "a /\ b" := ... (format "...", format "latex" "#1 \wedge #2"). - a posteriori: Format Notation "a /\ b" "latex" "#1 \wedge #2".
* Add syntax [id]: to apply tactic to goal named id.Gravatar Hugo Herbelin2014-09-12
|
* Factorize the parsing rules of [Record] and the other kind of type definitions.Gravatar Arnaud Spiwack2014-09-04
| | | | They were almost identical, except some unused misplaced coercion symbol in the non-[Record] rule.
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
| | | Dead code formerly used by the now defunct [autoinstances].
* Add a [Variant] declaration which allows to write non-recursive variant types.Gravatar Arnaud Spiwack2014-09-04
| | | | Just like the [Record] keyword allows only non-recursive records.
* Fixing bug #3493.Gravatar Pierre-Marie Pédrot2014-08-27
| | | | Coq now accepts the [Universes u1 ... un] syntax.
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
|
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
| | | | | par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2).
* Adding a new "Locate Term" command, distinct from the raw "Locate" command.Gravatar Pierre-Marie Pédrot2014-07-21
| | | | | | | | The new Term version has essentially the same behaviour as the old "Locate", while the new raw searches for all types of objects. Also code merging with the "Locate Ltac". Fixes bug #3380.
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
|
* Fix bug #3289Gravatar Matthieu Sozeau2014-06-11
|
* Remove the syntax [Vernac1. Vernac2. … Vernacn. ].Gravatar Arnaud Spiwack2014-06-06
| | | | | | | | It grouped a list of vernac commands as a single one. It was undocumented and unused (and apparently unusable, because the intermediate '.' seem to be parsed as end of phrases by the interfaces). The main application could be to group the commands for Time. There is room for such an application in the syntax, but I unplugged the syntax for the time being. The syntax would conflict with the use of a standalone dispatching tactical [ t1 | t2 | … | tn ]. I took the opportunity to separate the code dedicated to lists of commands in a separate type from vernac_expr.
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | A quick and dirty approach to private inductive types Types for which computable functions are provided, but pattern-matching is disallowed. This kind of type can be used to simulate simple forms of higher inductive types, with convertibility for applications of the inductive principle to 0-constructors Conflicts: intf/vernacexpr.mli kernel/declarations.ml kernel/declarations.mli kernel/entries.mli kernel/indtypes.ml library/declare.ml parsing/g_vernac.ml4 plugins/funind/glob_term_to_relation.ml pretyping/indrec.ml pretyping/tacred.mli printing/ppvernac.ml toplevel/vernacentries.ml Conflicts: kernel/declarations.mli kernel/declareops.ml kernel/indtypes.ml kernel/modops.ml
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 17:08:33 +0000