aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacenv.ml
Commit message (Expand)AuthorAge
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Granting wish #4048: Locate Ltac prints the source of redefined Ltac.Gravatar Pierre-Marie Pédrot2015-05-15
* Adding a test to check whether two tactic notations conflict.Gravatar Pierre-Marie Pédrot2015-05-11
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixing CAMLP4 compilation.Gravatar Pierre-Marie Pédrot2014-12-16
* Fixing nice printing of error reporting with ml tactics bound to ltac names.Gravatar Hugo Herbelin2014-10-01
* Fixing bug #2818.Gravatar Pierre-Marie Pédrot2014-09-03
* Useless hooks in Tacintern.Gravatar Pierre-Marie Pédrot2014-09-03
* Code simplification in Tacenv.Gravatar Pierre-Marie Pédrot2014-09-03
* Getting rid of atomic tactics in Tacenv.Gravatar Pierre-Marie Pédrot2014-08-31
* Moving code of tactic interpretation from Tacenv to Vernacentries.Gravatar Pierre-Marie Pédrot2014-08-31
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Removing the "constructor" tactic from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
* Code cleaning in Tacenv.Gravatar Pierre-Marie Pédrot2014-07-27
* Qualified ML tactic names. The plugin name is used to discriminateGravatar Pierre-Marie Pédrot2014-07-27
* Useless keeping of dirpath in tactic aliases.Gravatar Pierre-Marie Pédrot2014-06-30
* 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
* Allowing Ltac definitions that may be unusable because of a built-inGravatar Pierre-Marie Pédrot2014-05-21
* Moving left & right tactics out of the AST.Gravatar Pierre-Marie Pédrot2014-05-21
* Moving argument-free tactics out of the AST into a dedicatedGravatar Pierre-Marie Pédrot2014-05-16
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* Fix bug#2080: error message on Ltac name clash with primitive tacticsGravatar xclerc2014-01-10
* Centralizing the Ltac-defining functions in Tacenv.Gravatar ppedrot2013-11-10
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-10
* Revert the previous commit. It broke Coq compilation.Gravatar ppedrot2013-11-09
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 15:06:37 +0000