aboutsummaryrefslogtreecommitdiff
path: root/grammar/tacextend.ml4
AgeCommit message (Collapse)Author
2016-06-01Yet another Makefile reform : a unique phase without nasty make tricksPierre Letouzey
We're back to a unique build phase (as before e372b72), but without relying on the awkward include-deps-failed-lets-retry feature of make. Since PMP has made grammar/ self-contained, we could now build grammar.cma in a rather straightforward way, no need for a specific sub-call to $(MAKE) for that. The dependencies between files of grammar/ are stated explicitely, since .d files aren't fully available initially. Some Makefile simplifications, for instance remove the CAMLP4DEPS shell horror. Instead, we generalize the use of two different filename extensions : - a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp) - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo), except coqide_main.ml4 and its specific rule Note that we do not generate .ml4.d anymore (thanks to the .mlp vs. .ml4 dichotomy)
2016-05-31Making the grammar/ folder independent from the other ones.Pierre-Marie Pédrot
2016-05-14Hack in TACTIC EXTEND to maintain the 8.5 behaviour on badly designed arguments.Pierre-Marie Pédrot
Since TACTIC EXTEND relies on the usual tactic notation mechanism, the interpretation of an ML tactic first goes through a TacAlias node. This means that variables bound by the notation overwrite those of the current environment. It turns out to be problematic for badly designed arguments that close over variables of the environment, e.g. glob_constr, because the variables used at interpretation time are now different from the ones of parsing time. Ideally, those arguments should return a closure made of the inner argument together with the Ltac environment they were defined in. Unluckily, this would need some important changes in their design. Most notably, most of ssreflect ARGUMENT EXTEND actually create such closed arguments. In order to emulate the old behaviour, we rather use a hack by prefixing ML-bound variables by a character that is not accessible from user-side.
2016-04-24Higher-level API for tactic notations.Pierre-Marie Pédrot
2016-04-24Factorizing the declaration of ML notation printing in Tacentries.Pierre-Marie Pédrot
2016-03-20Moving the tactic related code from Metasyntax to a new file.Pierre-Marie Pédrot
2016-03-19EXTEND macros use their own internal representations.Pierre-Marie Pédrot
2016-03-19Do not keep the argument type in ExtNonTerminal.Pierre-Marie Pédrot
2016-03-19Further reducing the dependencies of the EXTEND macros.Pierre-Marie Pédrot
2016-03-18Making the EXTEND macros almost self-contained.Pierre-Marie Pédrot
2016-03-18ARGUMENT EXTEND made of only one entry share the same grammar.Pierre-Marie Pédrot
This fixes parsing conflicts with the [fix ... with] tactic.
2016-03-17Removing the special status of generic arguments defined by Coq itself.Pierre-Marie Pédrot
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.
2016-03-17Reducing the number of modules linked in grammar.cma.Pierre-Marie Pédrot
2016-02-24Removing the Q_coqast module.Pierre-Marie Pédrot
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.
2016-02-01Infering atomic ML entries from their grammar.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-17ML extensions use untyped representation of user entries.Pierre-Marie Pédrot
2016-01-16Tactic notation printing accesses all the token data.Pierre-Marie Pédrot
2016-01-02Simplification of grammar_prod_item type.Pierre-Marie Pédrot
Actually the identifier was never used and just carried along.
2016-01-02Proper datatype for EXTEND syntax tokens.Pierre-Marie Pédrot
2015-12-21Using dynamic values in tactic evaluation.Pierre-Marie Pédrot
2015-10-27Type-safe Egramml.grammar_prod_item.Pierre-Marie Pédrot
2015-10-27Finer type for Pcoq.interp_entry_name.Pierre-Marie Pédrot
2015-10-27Indexing existentially quantified entries returned by interp_entry_name.Pierre-Marie Pédrot
2015-10-26Pcoq entries are given a proper module.Pierre-Marie Pédrot
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.
2015-10-21Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.Pierre-Marie Pédrot
2015-07-02Merge branch 'v8.5' into trunkMaxime Dénès
2015-06-29Code documentation of the TACTIC/VERNAC EXTEND macros.Pierre-Marie Pédrot
2015-05-15Merge v8.5 into trunkHugo Herbelin
Conflicts: tactics/eauto.ml4 (merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
2015-05-08A more user-friendly naming of variables of ltac names defined byHugo Herbelin
TACTIC EXTEND (based on user-given name).
2015-01-27Tentative fix for bug #3957.Pierre-Marie Pédrot
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.
2015-01-23Splitting ML tactics in one function per grammar entry.Pierre-Marie Pédrot
Furthermore, ML tactic dispatch is not done according to the type of its argument anymore.
2015-01-21Embedding the index of the ML tactic entry in the Tacexpr AST.Pierre-Marie Pédrot
This will allow to get rid of the fragile mechanism of discriminating which entry to call depending on the dynamic type of its arguments.
2015-01-12Update headers.Maxime Dénès
2014-12-16Fixing CAMLP4 compilation.Pierre-Marie Pédrot
2014-11-08Continuing 3741c46fe134 on reporting ltac error.Hugo Herbelin
- 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>)?
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
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.
2014-08-31Moving code of tactic interpretation from Tacenv to Vernacentries.Pierre-Marie Pédrot
This allows to directly register globtactics in the Tacenv API, without having to resort to any internalization function.
2014-08-18Moving the TacExtend node from atomic to plain tactics.Pierre-Marie Pédrot
Also taking advantage of the change to rename it into TacML. Ultimately should allow ML tactic to return values.
2014-07-27Qualified ML tactic names. The plugin name is used to discriminatePierre-Marie Pédrot
potentially conflicting tactics names from different plugins.
2014-05-24Fixing TACTIC EXTEND for arguments-free tactics that may modify the wholePierre-Marie Pédrot
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.
2014-05-20Tactics declared through TACTIC EXTEND that are of the formPierre-Marie Pédrot
"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.
2014-05-17Fixing Camlp4 compilationPierre-Marie Pédrot
2014-05-16Tactics defined through TACTIC EXTEND that are only defined as a string doPierre-Marie Pédrot
not create grammar and printing rules anymore, they define Ltac entries in the module that declares them instead.
2014-05-12Now parsing rules of ML-declared tactics are only made available after thePierre-Marie Pédrot
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.
2014-05-12Moving the ML tactic extension mechanism to a Libobject-based one.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
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.
2014-02-05Tactic extensions do not need to be classified by the STM, asPierre-Marie Pédrot
they never produce a VernacExtend entry.
2013-11-10Centralizing the Ltac-defining functions in Tacenv.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17080 85f007b7-540e-0410-9357-904b9bb8a0f7