index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
tacintern.mli
Age
Commit message (
Expand
)
Author
2016-03-21
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2016-01-02
Reduce dependencies of interface files.
Guillaume Melquiond
2015-02-27
Removing the unused field ltacrecvars of tactic internalization.
Pierre-Marie Pédrot
2015-01-12
Update headers.
Maxime Dénès
2014-09-03
Useless hooks in Tacintern.
Pierre-Marie Pédrot
2014-08-31
Getting rid of atomic tactics in Tacenv.
Pierre-Marie Pédrot
2014-07-27
Qualified ML tactic names. The plugin name is used to discriminate
Pierre-Marie Pédrot
2014-03-05
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2013-12-17
Removing the need of evarmaps in constr internalization.
Pierre-Marie Pédrot
2013-11-10
Centralizing the Ltac-defining functions in Tacenv.
ppedrot
2013-08-03
Replacing an association list by a map in globalizing environment.
ppedrot
2013-06-27
Removed the distinction between generic Ltac vars and Let/Intro
ppedrot
2013-06-21
Splitted up Genarg in four different levels:
ppedrot
2013-06-18
Removing the various glob/subst/interp registering functions for
ppedrot
2013-06-18
Now glob_sign and interp_sign only depend on structures defined
ppedrot
2013-05-29
Make ist (interp_sign) available to TACTIC EXTEND code
gareuselesinge
2012-12-14
Modulification of identifier
ppedrot
2012-10-16
Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp
letouzey
