index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
/
genintern.mli
Commit message (
Expand
)
Author
Age
*
[api] Misctypes removal: move Tactypes to proofs
Emilio Jesus Gallego Arias
2018-06-12
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Allowing to pass arbitrary data in internalization environments.
Pierre-Marie Pédrot
2017-05-03
*
Untangling Tacexpr from lower strata.
Pierre-Marie Pédrot
2016-09-15
*
Generalizing the notion of constr substitution to generic arguments.
Pierre-Marie Pédrot
2016-09-15
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Removing the unused field ltacrecvars of tactic internalization.
Pierre-Marie Pédrot
2015-02-27
*
Update headers.
Maxime Dénès
2015-01-12
*
Removing the need of evarmaps in constr internalization.
Pierre-Marie Pédrot
2013-12-17
*
Replacing an association list by a map in globalizing environment.
ppedrot
2013-08-03
*
Removed the distinction between generic Ltac vars and Let/Intro
ppedrot
2013-06-27
*
Splitted up Genarg in four different levels:
ppedrot
2013-06-21