aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* Fixing CAMLP4 compilation.Gravatar Pierre-Marie Pédrot2014-12-16
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* About now accepts hypothesis names and goal selector.Gravatar Pierre Courtieu2014-12-15
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Removing a unused boolean in the TacMove node of tacexpr AST.Gravatar Pierre-Marie Pédrot2014-11-09
* Fixing bugs #3723 and #3787 (reinitialization of camlp5 empty levels)Gravatar Hugo Herbelin2014-11-06
* Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".Gravatar Hugo Herbelin2014-11-02
* Add [Info] command.Gravatar Arnaud Spiwack2014-11-01
* Reorganization of the test for generic selection of occurrences inGravatar Hugo Herbelin2014-10-31
* Dead codeGravatar Hugo Herbelin2014-10-27
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Emit a warning for void Arguments statement (Close 3713)Gravatar Enrico Tassi2014-10-13
* Parsing of "?[" as two tokens (makes ssr compile).Gravatar Enrico Tassi2014-10-13
* Fixing #3687 (inconsistent lexer state after a bullet).Gravatar Hugo Herbelin2014-10-07
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
* Using an or_var rather than the hack with loc for coding a pure identGravatar Hugo Herbelin2014-09-24
* Add a "Hint Mode ref (+ | -)*" hint for setting a global modeGravatar Matthieu Sozeau2014-09-15
* Checking typability of evar instances. Using ";" to separate bindingsGravatar Hugo Herbelin2014-09-13
* Add syntax [id]: to apply tactic to goal named id.Gravatar Hugo Herbelin2014-09-12
* Parsing evar instances.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* VernacExtend does not dispatch on type anymore.Gravatar Pierre-Marie Pédrot2014-09-10
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Factorize the parsing rules of [Record] and the other kind of type definitions.Gravatar Arnaud Spiwack2014-09-04
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
* Add a [Variant] declaration which allows to write non-recursive variant types.Gravatar Arnaud Spiwack2014-09-04
* Removing [revert] tactic from the AST.Gravatar Pierre-Marie Pédrot2014-09-02
* Moving the decompose tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-09-01
* Fixing bug #3493.Gravatar Pierre-Marie Pédrot2014-08-27
* Removing a unused legacy parsing rule.Gravatar Pierre-Marie Pédrot2014-08-24
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
* Moving the TacAlias node out of atomic tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Fixing parsing of bullets after a "...".Gravatar Hugo Herbelin2014-08-12
* Removing simple induction / destruct from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
* Instead of relying on a trick to make the constructor tactic parse, putGravatar Pierre-Marie Pédrot2014-08-07
* Removing the "constructor" tactic from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
* Removing "intros untils" from the AST.Gravatar Pierre-Marie Pédrot2014-08-06
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* Adding a syntax "enough" for the variant of "assert" with the order ofGravatar Hugo Herbelin2014-08-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-28 19:49:19 +0000