index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
interp
/
genintern.mli
Age
Commit message (
Expand
)
Author
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2018-10-31
Fixes rest of #3468 (tactic-in-term was not respecting scopes).
Hugo Herbelin
2018-06-12
[api] Misctypes removal: move Tactypes to proofs
Emilio Jesus Gallego Arias
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-05-03
Allowing to pass arbitrary data in internalization environments.
Pierre-Marie Pédrot
2016-09-15
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-01-20
Update copyright headers.
Maxime Dénès
2015-02-27
Removing the unused field ltacrecvars of tactic internalization.
Pierre-Marie Pédrot
2015-01-12
Update headers.
Maxime Dénès
2013-12-17
Removing the need of evarmaps in constr internalization.
Pierre-Marie Pédrot
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
