aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacenv.ml
Commit message (Expand)AuthorAge
* Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Separation of concern in TacAlias API.Gravatar Pierre-Marie Pédrot2016-01-02
* | Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-01
|\|
| * Granting wish #4048: Locate Ltac prints the source of redefined Ltac.Gravatar Pierre-Marie Pédrot2015-05-15
* | Merge v8.5 into trunkGravatar Hugo Herbelin2015-05-15
|\|
| * Adding a test to check whether two tactic notations conflict.Gravatar Pierre-Marie Pédrot2015-05-11
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-05-05
|\|
| * Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-10
|\|
| * Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* | Splitting ML tactics in one function per grammar entry.Gravatar Pierre-Marie Pédrot2015-01-23
* | Embedding the index of the ML tactic entry in the Tacexpr AST.Gravatar Pierre-Marie Pédrot2015-01-21
|/
* 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-30 13:02:53 +0000