aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar/tacextend.ml4
Commit message (Collapse)AuthorAge
* Moving the tactic related code from Metasyntax to a new file.Gravatar Pierre-Marie Pédrot2016-03-20
|
* EXTEND macros use their own internal representations.Gravatar Pierre-Marie Pédrot2016-03-19
|
* Do not keep the argument type in ExtNonTerminal.Gravatar Pierre-Marie Pédrot2016-03-19
|
* Further reducing the dependencies of the EXTEND macros.Gravatar Pierre-Marie Pédrot2016-03-19
|
* Making the EXTEND macros almost self-contained.Gravatar Pierre-Marie Pédrot2016-03-18
|
* ARGUMENT EXTEND made of only one entry share the same grammar.Gravatar Pierre-Marie Pédrot2016-03-18
| | | | This fixes parsing conflicts with the [fix ... with] tactic.
* Removing the special status of generic arguments defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
| | | | | | | | This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They now have to be reachable in the ML code. Note that this has some consequences, as the previous macro was potentially mixing grammar entries and arguments as long as their name was the same. Now, each genarg comes with its grammar instead, so there is no way to abuse the macro.
* Reducing the number of modules linked in grammar.cma.Gravatar Pierre-Marie Pédrot2016-03-17
|
* Removing the Q_coqast module.Gravatar Pierre-Marie Pédrot2016-02-24
| | | | | | It implemented the quotation logic of terms and tactics, although it was mostly obsolete. With quotations gone, it is now useless and thus removed. I fundamentally doubt that anyone hardly depends on this out there.
* Infering atomic ML entries from their grammar.Gravatar Pierre-Marie Pédrot2016-02-01
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | ML extensions use untyped representation of user entries.Gravatar Pierre-Marie Pédrot2016-01-17
| |
* | Tactic notation printing accesses all the token data.Gravatar Pierre-Marie Pédrot2016-01-16
| |
* | Simplification of grammar_prod_item type.Gravatar Pierre-Marie Pédrot2016-01-02
| | | | | | | | Actually the identifier was never used and just carried along.
* | Proper datatype for EXTEND syntax tokens.Gravatar Pierre-Marie Pédrot2016-01-02
| |
* | Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
| |
* | Type-safe Egramml.grammar_prod_item.Gravatar Pierre-Marie Pédrot2015-10-27
| |
* | Finer type for Pcoq.interp_entry_name.Gravatar Pierre-Marie Pédrot2015-10-27
| |
* | Indexing existentially quantified entries returned by interp_entry_name.Gravatar Pierre-Marie Pédrot2015-10-27
| |
* | Pcoq entries are given a proper module.Gravatar Pierre-Marie Pédrot2015-10-26
| | | | | | | | | | | | | | | | | | | | | | Entries defined in the Pcoq AST of symbols must be marshallable, because they are present in the libstack. Yet, CAMLP4/5 entries are not marshallable as they contain functional values. This is why the Pcoq module used a pair [string * string] to describe entries. It is obviously type-unsafe, so we define a new abstract type in its own module. There is a little issue though, which is that our entries and CAMLP4/5 entries must be kept synchronized through an association table. The Pcoq module tries to maintain this invariant.
* | Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.Gravatar Pierre-Marie Pédrot2015-10-21
| |
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-07-02
|\|
| * Code documentation of the TACTIC/VERNAC EXTEND macros.Gravatar Pierre-Marie Pédrot2015-06-29
| |
* | Merge v8.5 into trunkGravatar Hugo Herbelin2015-05-15
|\| | | | | | | | | | | | | Conflicts: tactics/eauto.ml4 (merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
| * A more user-friendly naming of variables of ltac names defined byGravatar Hugo Herbelin2015-05-08
| | | | | | | | TACTIC EXTEND (based on user-given name).
* | Tentative fix for bug #3957.Gravatar Pierre-Marie Pédrot2015-01-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Now that ML tactics are not dispatched according to the type of their arguments anymore, one has to take care of the way potentially atomic tactics are handled. This patch ensures that the atomic tactics generated by the TACTIC EXTEND macro have the right length and the right order. There may be very rare trouble if two ML tactics in the same entry are of the form "foo" x1 ... xn "foo" y1 ... ym where all xi and yi may be empty. I doubt that the legacy implementation behaved well in this case anyway.
* | Splitting ML tactics in one function per grammar entry.Gravatar Pierre-Marie Pédrot2015-01-23
| | | | | | | | | | Furthermore, ML tactic dispatch is not done according to the type of its argument anymore.
* | Embedding the index of the ML tactic entry in the Tacexpr AST.Gravatar Pierre-Marie Pédrot2015-01-21
|/ | | | | This will allow to get rid of the fragile mechanism of discriminating which entry to call depending on the dynamic type of its arguments.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Fixing CAMLP4 compilation.Gravatar Pierre-Marie Pédrot2014-12-16
|
* Continuing 3741c46fe134 on reporting ltac error.Gravatar Hugo Herbelin2014-11-08
| | | | | | | | | | | | | | | | | | | | | | | | | - Do use the flag for_ml for distinguishing coq level and ml level ltac definitions. - Skip ML call from the trace. There are still differences from 8.4 and trunk. For instance on: Ltac f x := refine x. Goal False. f I. 8.4 says: In nested Ltac calls to "f" and "x" (with x:=I), last term evaluation failed. Error: The term "I" has type "True" while it is expected to have type "False". trunk says: In nested Ltac calls to "f" and "refine <genarg:uconstr>", last call failed. Error: The term "I" has type "True" while it is expected to have type "False". Maybe we would like a mix of both (besides the printing of a non-elegant "<genarg:uconstr>)?
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
| | | | | | | | | | | 1. Proofview.Goal.enter into Proofview.Goal.nf_enter. 2. Proofview.Goal.raw_enter into Proofview.Goal.enter. 3. Proofview.Goal.goals -> Proofview.Goals.nf_goals 4. Proofview.Goal.raw_goals -> Proofview.Goals.goals 5. Ftactic.goals -> Ftactic.nf_goals 6. Ftactic.raw_goals -> Ftactic.goals This is more uniform with the other functions of Coq.
* Moving code of tactic interpretation from Tacenv to Vernacentries.Gravatar Pierre-Marie Pédrot2014-08-31
| | | | | This allows to directly register globtactics in the Tacenv API, without having to resort to any internalization function.
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
| | | | | Also taking advantage of the change to rename it into TacML. Ultimately should allow ML tactic to return values.
* Qualified ML tactic names. The plugin name is used to discriminateGravatar Pierre-Marie Pédrot2014-07-27
| | | | potentially conflicting tactics names from different plugins.
* Fixing TACTIC EXTEND for arguments-free tactics that may modify the wholeGravatar Pierre-Marie Pédrot2014-05-24
| | | | | | | | proof. Indeed, computing an empty list of arguments triggered a Proofview.Goal.enter, which broke tactics like [shelve_unifiable]. This does not fix this particular tactic though, because the Ltac interpreter still enters the goal when calling a Ltac reference.
* Tactics declared through TACTIC EXTEND that are of the formGravatar Pierre-Marie Pédrot2014-05-20
| | | | | | | | | "foobar" constr(x1) ... constr(xn) are now defined as pure Ltac definitions, and do not add grammar nor printing rules. This partially relies on a hack consisting in retrieving the arguments in the tactic environment rather than as directly passed to the TacExtend node.
* Fixing Camlp4 compilationGravatar Pierre-Marie Pédrot2014-05-17
|
* Tactics defined through TACTIC EXTEND that are only defined as a string doGravatar Pierre-Marie Pédrot2014-05-16
| | | | | not create grammar and printing rules anymore, they define Ltac entries in the module that declares them instead.
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
| | | | | | | | | | | | | corresponding Declare ML Module command. This changes essentially two things: 1. ML plugins are forced to use the DECLARE PLUGIN statement before any TACTIC EXTEND statement. The plugin name must be exactly the string passed to the Declare ML Module command. 2. ML tactics are only made available after the Coq module that does the corresponding Declare ML Module is imported. This may break a few things, as it already broke quite some uses of omega in the stdlib.
* Moving the ML tactic extension mechanism to a Libobject-based one.Gravatar Pierre-Marie Pédrot2014-05-12
|
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
| | | | | | | | With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
* Tactic extensions do not need to be classified by the STM, asGravatar Pierre-Marie Pédrot2014-02-05
| | | | they never produce a VernacExtend entry.
* Centralizing the Ltac-defining functions in Tacenv.Gravatar ppedrot2013-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17080 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-10
| | | | | | | | | Instead of putting the body directly in the AST, we register it in a table. This time it should work properly. Tactic notation are given kernel names to ensure the unicity of their contents. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17079 85f007b7-540e-0410-9357-904b9bb8a0f7
* CList.factorize_left with a parametric equalityGravatar letouzey2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16923 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vernac classification streamlined (handles VERNAC EXTEND)Gravatar gareuselesinge2013-08-08
| | | | | | | | | | | | | | | | | | | | | | | The warning output by vernacextend when the classifier is missing is the documentation of this commit: Warning: Vernac entry "Foo" misses a classifier. A classifier is a function that returns an expression of type vernac_classification (see Vernacexpr). You can: - Use '... EXTEND Foo CLASSIFIED AS QUERY ...' if the new vernacular command does not alter the system state; - Use '... EXTEND Foo CLASSIFIED AS SIDEFF ...' if the new vernacular command alters the system state but not the parser nor it starts a proof or ends one; - Use '... EXTEND Foo CLASSIFIED BY f ...' to specify a global function f. The function f will be called passing "Foo" as the only argument; - Add a specific classifier in each clause using the syntax: '[...] => [ f ] -> [...]'. Specific classifiers have precedence over global classifiers. Only one classifier is called. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16680 85f007b7-540e-0410-9357-904b9bb8a0f7
* Expurgating the useless difference between List0 and List1 at theGravatar ppedrot2013-07-05
| | | | | | | | | | level of generic arguments. This only matters at parsing time. TODO: the current status is not satisfactory enough, as rule emptyness is still decided w.r.t. generic arguments. This should be done on a grammar entry basis instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16617 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing the use of leveled tactics wit_tacticn. It is now handledGravatar ppedrot2013-07-02
| | | | | | | | | | | | through a unique generic argument, and the level is only considered at parsing time. This may introduce unnecessary parentheses in Ltac printing though, as every tactic argument is collapsed at the lowest level. I assume this does not matter that much, and anyway Ltac printing is quite bugged as of today. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16616 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 21:53:35 +0000