aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacintern.mli
Commit message (Expand)AuthorAge
* Useless hooks in Tacintern.Gravatar Pierre-Marie Pédrot2014-09-03
* Getting rid of atomic tactics in Tacenv.Gravatar Pierre-Marie Pédrot2014-08-31
* Qualified ML tactic names. The plugin name is used to discriminateGravatar Pierre-Marie Pédrot2014-07-27
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Removing the need of evarmaps in constr internalization.Gravatar Pierre-Marie Pédrot2013-12-17
* Centralizing the Ltac-defining functions in Tacenv.Gravatar ppedrot2013-11-10
* Replacing an association list by a map in globalizing environment.Gravatar ppedrot2013-08-03
* Removed the distinction between generic Ltac vars and Let/IntroGravatar ppedrot2013-06-27
* 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