aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacintern.mli
Commit message (Expand)AuthorAge
* Splitted up Genarg in four different levels:Gravatar ppedrot2013-06-21
* Removing the various glob/subst/interp registering functions forGravatar ppedrot2013-06-18
* Now glob_sign and interp_sign only depend on structures definedGravatar ppedrot2013-06-18
* Make ist (interp_sign) available to TACTIC EXTEND codeGravatar gareuselesinge2013-05-29
* Modulification of identifierGravatar ppedrot2012-12-14
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16