aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar/argextend.ml4
Commit message (Collapse)AuthorAge
* Yet another Makefile reform : a unique phase without nasty make tricksGravatar Pierre Letouzey2016-06-01
| | | | | | | | | | | | | | | | | | | | 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)
* Making the grammar/ folder independent from the other ones.Gravatar Pierre-Marie Pédrot2016-05-31
|
* Removing the Entry module now that rules need not be marshalled.Gravatar Pierre-Marie Pédrot2016-05-10
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\
| * Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
| |
* | Interpretation function can return any untyped value.Gravatar Pierre-Marie Pédrot2016-05-04
| |
* | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
| |
* | Adding warnings for inferrable *_TYPED AS clauses.Gravatar Pierre-Marie Pédrot2016-04-12
| |
* | Allowing optional RAW_TYPED and GLOB_TYPED clauses in ARGUMENT EXTEND.Gravatar Pierre-Marie Pédrot2016-04-12
| |
* | Warning for redundant TYPED AS clauses.Gravatar Pierre-Marie Pédrot2016-04-12
| |
* | Allowing simple ARGUMENT EXTEND not to mention their self type.Gravatar Pierre-Marie Pédrot2016-04-12
| | | | | | | | | | The TYPED AS clause was useless when defining a fresh generic argument. Instead of having to write it mandatorily, we simply make it optional.
* | Allowing the presence of TYPED AS in specialized ARGUMENT EXTEND.Gravatar Pierre-Marie Pédrot2016-04-12
| | | | | | | | | | This allows to use the ARGUMENT EXTEND macro while sharing the same toplevel dynamic representation as another argument.
* | Moving the code handling tactic notations to Tacentries.Gravatar Pierre-Marie Pédrot2016-03-31
| |
* | 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
| |
* | Do not export entry_key from Pcoq anymore.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.
* | Removing the special status of generic entries defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
| | | | | | | | | | | | | | | | | | | | | | The ARGUMENT EXTEND macro was discriminating between parsing entries known statically, i.e. defined in Pcoq and unknown entires. Although simplifying a bit the life of the plugin writer, it made actual interpretation difficult to predict and complicated the code of the ARGUMENT EXTEND macro. After this patch, all parsing entries and generic arguments used in an ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding a few more "open Pcoq.X" and "open Constrarg" here and there.
* | Adding a universe argument to Pcoq.create_generic_entry.Gravatar Pierre-Marie Pédrot2016-03-17
| |
* | Removing the registering of default values for generic arguments.Gravatar Pierre-Marie Pédrot2016-03-17
| |
* | Reducing the number of modules linked in grammar.cma.Gravatar Pierre-Marie Pédrot2016-03-17
| |
| * Fixing bug #4608: Anomaly "output_value: abstract value (outside heap)".Gravatar Pierre-Marie Pédrot2016-03-05
| | | | | | | | | | | | | | The ARGUMENT EXTEND statement was wrongly using a CompatLoc instead of a Loc, and this was not detected by typing "thanks" to the Gram.action magic. When using CAMLP4, this was wreaking havoc at runtime, but not when using CAMLP5, as the locations where sharing the same representation.
* | All arguments defined through ARGUMENT EXTEND declare a tactic scope.Gravatar Pierre-Marie Pédrot2016-03-04
| | | | | | | | | | Amongs other things, it kind of fixes bug #4492, even though you cannot really take advantage of the parsed data for now.
* | 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
| |
* | Removing constr generic argument.Gravatar Pierre-Marie Pédrot2016-01-14
| |
* | Removing ident and var generic arguments.Gravatar Pierre-Marie Pédrot2016-01-14
| |
* | Monotonizing Ftactic.Gravatar Pierre-Marie Pédrot2016-01-08
| |
* | Proper datatype for EXTEND syntax tokens.Gravatar Pierre-Marie Pédrot2016-01-02
| |
* | Implementing non-focussed generic arguments.Gravatar Pierre-Marie Pédrot2015-12-28
| | | | | | | | | | | | | | Kind of enhances the situation of bug #4409. Now arguments can be interpreted globally or focussedly in a dynamic fashion because the interpretation function returns a Ftactic.t. The bug is not fixed yet because we should tweak the interpretation of tactic arguments.
* | Removing the special status of open_constr generic argument.Gravatar Pierre-Marie Pédrot2015-12-28
| | | | | | | | | | We also intepret it at toplevel as a true constr and push the resulting evarmap in the current state.
* | ARGUMENT EXTEND shares the toplevel representation when possible.Gravatar Pierre-Marie Pédrot2015-12-21
| |
* | Removing ad-hoc interpretation rules for tactic notations and their genarg.Gravatar Pierre-Marie Pédrot2015-12-21
| | | | | | | | | | | | Now that types can share the same dynamic representation, we do not have to transtype the topelvel values dynamically and just take advantage of the standard interpretation function.
* | Removing the now useless genarg generic argument.Gravatar Pierre-Marie Pédrot2015-12-21
| |
* | Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
| |
* | Getting rid of some hardwired generic arguments.Gravatar Pierre-Marie Pédrot2015-12-17
| |
* | Type-safe Argextend.Gravatar Pierre-Marie Pédrot2015-10-28
| |
* | 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.prod_entry_key now uses a GADT to statically enforce typedness.Gravatar Pierre-Marie Pédrot2015-10-21
|/
* Update headers.Gravatar Maxime Dénès2015-01-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.
* Removing the useless pattern ident genarg.Gravatar Pierre-Marie Pédrot2013-12-19
|
* Removing RefArgType generic argument.Gravatar Pierre-Marie Pédrot2013-12-01
|
* Getting rid of casted_open_constr. It was only used by theGravatar Pierre-Marie Pédrot2013-11-30
| | | | | | | | | | | | | | | | | refine tactic, which now uses plain glob_constr's. Now there is no real need to depend on goal when interpreting genargs. Possible minor incompatibilities: 1. The interpretation of glob_constr to constr is now done by Goal.constr_of_raw, which may be slightly dumbier than the dedicated Tacinterp.interp_open_constr which tries harder. Stdlib and test-suite do go through, though. 2. I had to change the parsing level of wit_glob in Extraargs from lconstr to constr. It may break ML notations using glob, but as they are only used inside Coq code and all well-parenthezised, it should be OK.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 01:26:46 +0000