aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacenv.ml
AgeCommit message (Expand)Author
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-02Separation of concern in TacAlias API.Pierre-Marie Pédrot
2015-12-21Using dynamic values in tactic evaluation.Pierre-Marie Pédrot
2015-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2015-05-15Granting wish #4048: Locate Ltac prints the source of redefined Ltac.Pierre-Marie Pédrot
2015-05-15Merge v8.5 into trunkHugo Herbelin
2015-05-11Adding a test to check whether two tactic notations conflict.Pierre-Marie Pédrot
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-02-10Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-23Splitting ML tactics in one function per grammar entry.Pierre-Marie Pédrot
2015-01-21Embedding the index of the ML tactic entry in the Tacexpr AST.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-16Fixing CAMLP4 compilation.Pierre-Marie Pédrot
2014-10-01Fixing nice printing of error reporting with ml tactics bound to ltac names.Hugo Herbelin
2014-09-03Fixing bug #2818.Pierre-Marie Pédrot
2014-09-03Useless hooks in Tacintern.Pierre-Marie Pédrot
2014-09-03Code simplification in Tacenv.Pierre-Marie Pédrot
2014-08-31Getting rid of atomic tactics in Tacenv.Pierre-Marie Pédrot
2014-08-31Moving code of tactic interpretation from Tacenv to Vernacentries.Pierre-Marie Pédrot
2014-08-18Moving the TacExtend node from atomic to plain tactics.Pierre-Marie Pédrot
2014-08-07Removing the "constructor" tactic from the AST.Pierre-Marie Pédrot
2014-07-27Code cleaning in Tacenv.Pierre-Marie Pédrot
2014-07-27Qualified ML tactic names. The plugin name is used to discriminatePierre-Marie Pédrot
2014-06-30Useless keeping of dirpath in tactic aliases.Pierre-Marie Pédrot
2014-06-06Moving the [split] tactic out of the AST.Pierre-Marie Pédrot
2014-06-02Removing symmetry from the atomic tactics.Pierre-Marie Pédrot
2014-05-21Allowing Ltac definitions that may be unusable because of a built-inPierre-Marie Pédrot
2014-05-21Moving left & right tactics out of the AST.Pierre-Marie Pédrot
2014-05-16Moving argument-free tactics out of the AST into a dedicatedPierre-Marie Pédrot
2014-05-12Now parsing rules of ML-declared tactics are only made available after thePierre-Marie Pédrot
2014-01-10Fix bug#2080: error message on Ltac name clash with primitive tacticsxclerc
2013-11-10Centralizing the Ltac-defining functions in Tacenv.ppedrot
2013-11-10Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-09Revert the previous commit. It broke Coq compilation.ppedrot
2013-11-09Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 05:32:20 +0000