aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_tactic.ml4
AgeCommit message (Expand)Author
2016-09-14Moving Ltac-specific parsing API to ltac/ folder.Pierre-Marie Pédrot
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-07-18Removing useless grammar entries. Fixes bug #4919.Pierre-Marie Pédrot
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Add and document match, fix and cofix reduction flags.Maxime Dénès
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-18Exporting a generic argument induction_arg. As a consequence,Hugo Herbelin
2016-06-18Adding eintros to respect the e- prefix policy.Hugo Herbelin
2016-06-16Fixing a mispelling coma -> comma.Hugo Herbelin
2016-06-16A stronger invariant on the syntax of TacAssert, what allows for aHugo Herbelin
2016-06-03Removing "rename" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "exact" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "intro" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "double induction" from the tactic AST.Pierre-Marie Pédrot
2016-06-01g_tactics : remove opt_bindings (2-line dead code)Pierre Letouzey
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-09Rename Lexer -> CLexer.Pierre-Marie Pédrot
2016-04-27Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Hugo Herbelin
2016-04-27Revert "Fixing a mispelling coma -> comma."Hugo Herbelin
2016-04-27Fixing a mispelling coma -> comma.Hugo Herbelin
2016-04-27In the short term, stronger invariant on the syntax of TacAssert, whatHugo Herbelin
2016-02-29Moving the "move" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "exists" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "symmetry" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "generalize dependent" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "clearbody" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "clear" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "cofix" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "fix" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-21Stronger invariants on the use of the introduction pattern (pat1,...,patn).Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2015-12-28Removing unused parsing entries.Pierre-Marie Pédrot
2015-12-28Removing the special status of open_constr generic argument.Pierre-Marie Pédrot
2015-12-25Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.mlHugo Herbelin
2015-12-24Removing auto from the tactic AST.Pierre-Marie Pédrot
2015-12-15Tactics: Generalizing the use of the experimental clearing modifier toHugo Herbelin
2015-12-10Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Hugo Herbelin
2015-12-05Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Hugo Herbelin
2015-12-02Improving syntax of pat/constr introduction pattern so thatHugo Herbelin
2015-12-02Dead code from August 2014 in apply in.Hugo Herbelin
2015-10-30Manually expand red_tactic so that notations do not break reduction tactics. ...Guillaume Melquiond
2015-10-29Manually expand the debugging versions of "trivial" and "auto". (Fix bug #4392)Guillaume Melquiond
2015-03-30grammar: export hypidentEnrico Tassi
2015-01-12Update headers.Maxime Dénès
2014-12-12Extend the syntax of simpl with a delta flag.Arnaud Spiwack
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-09Removing a unused boolean in the TacMove node of tacexpr AST.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:40:58 +0000