aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_tactic.ml4
Commit message (Expand)AuthorAge
* Removing unused parsing entries.Gravatar Pierre-Marie Pédrot2015-12-28
* Removing the special status of open_constr generic argument.Gravatar Pierre-Marie Pédrot2015-12-28
* Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.mlGravatar Hugo Herbelin2015-12-25
* Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24
* Tactics: Generalizing the use of the experimental clearing modifier toGravatar Hugo Herbelin2015-12-15
* Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Gravatar Hugo Herbelin2015-12-10
* Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Gravatar Hugo Herbelin2015-12-05
* Improving syntax of pat/constr introduction pattern so thatGravatar Hugo Herbelin2015-12-02
* Dead code from August 2014 in apply in.Gravatar Hugo Herbelin2015-12-02
* Manually expand red_tactic so that notations do not break reduction tactics. ...Gravatar Guillaume Melquiond2015-10-30
* Manually expand the debugging versions of "trivial" and "auto". (Fix bug #4392)Gravatar Guillaume Melquiond2015-10-29
* grammar: export hypidentGravatar Enrico Tassi2015-03-30
* Update headers.Gravatar Maxime Dénès2015-01-12
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
* 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
* Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".Gravatar Hugo Herbelin2014-11-02
* 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
* 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
* Using an or_var rather than the hack with loc for coding a pure identGravatar Hugo Herbelin2014-09-24
* 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
* 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 TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* 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
* 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
* Properly declare uconstr as an argument for TACTIC EXTEND.Gravatar Arnaud Spiwack2014-08-05
* Moving the [split] tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-06-06
* Removing symmetry from the atomic tactics.Gravatar Pierre-Marie Pédrot2014-06-02
* Fixing commit 9cef834. The parsing rules were generating an empty list,Gravatar Pierre-Marie Pédrot2014-05-26
* Complying with reference manual for the syntax of exists/eexists, i.e.Gravatar Hugo Herbelin2014-05-24
* Moving the "specialize" tactic out of the AST. Also removed an obsoleteGravatar Pierre-Marie Pédrot2014-05-22
* Removing useless use of metaids in tactic AST.Gravatar Pierre-Marie Pédrot2014-05-22
* Removing decompose record / sum from the tactic AST.Gravatar Pierre-Marie Pédrot2014-05-21
* Moving left & right tactics out of the AST.Gravatar Pierre-Marie Pédrot2014-05-21
* Moving (e)transitivity out of the AST.Gravatar Pierre-Marie Pédrot2014-05-20
* Tentative to add constr-using primitive tactics without grammar rules.Gravatar Pierre-Marie Pédrot2014-05-20
* Moving argument-free tactics out of the AST into a dedicatedGravatar Pierre-Marie Pédrot2014-05-16
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Closing bug #3260Gravatar Julien Forest2014-04-14
* Getting rid of casted_open_constr. It was only used by theGravatar Pierre-Marie Pédrot2013-11-30
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 14:18:19 +0000