aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar/q_util.mli
Commit message (Collapse)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Adding support for using grammar entries returning no value in EXTEND.Gravatar Hugo Herbelin2017-05-16
|
* [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
| | | | | | | | We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes.
* [cleanup] Change Id.t option to Name.t in TacFunGravatar Tej Chajed2017-02-16
|
* Making the grammar/ folder independent from the other ones.Gravatar Pierre-Marie Pédrot2016-05-31
|
* Hack in TACTIC EXTEND to maintain the 8.5 behaviour on badly designed arguments.Gravatar Pierre-Marie Pédrot2016-05-14
| | | | | | | | | | | | | | | | | | 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.
* Getting rid of the "_mods" parsing entry.Gravatar Pierre-Marie Pédrot2016-04-01
| | | | | | It was only used by setoid_ring for the Add Ring command, and was easily replaced by a dedicated argument. Moreover, it was of no use to tactic notations.
* Fixing compilation with old versions of CAMLP5.Gravatar Pierre-Marie Pédrot2016-03-19
|
* 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
|
* Making the EXTEND macros almost self-contained.Gravatar Pierre-Marie Pédrot2016-03-18
|
* 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 dead code in Q_util.Gravatar Pierre-Marie Pédrot2016-03-17
|
* 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.
* 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
| |
* | Proper datatype for EXTEND syntax tokens.Gravatar Pierre-Marie Pédrot2016-01-02
| |
* | 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.
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* place all files specific to camlp4 syntax extensions in grammar/Gravatar letouzey2012-05-29
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15387 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 05:51:15 +0000