index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
interp
/
genintern.ml
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-11-01
Fix FIXME: use OCaml 4.02 generative functors when available.
Gaëtan Gilbert
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-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2016-01-17
Getting rid of the awkward unpack mechanism from Genarg.
Pierre-Marie Pédrot
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-08-29
Simplification of Genarg unpackers.
Pierre-Marie Pédrot
2014-03-05
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-01-19
Adding a default object to generic argument registering mechanism.
Pierre-Marie Pédrot
2013-12-17
Removing the need of evarmaps in constr internalization.
Pierre-Marie Pédrot
2013-11-27
Adding the necessary hooks to handle tactics in terms.
Pierre-Marie Pédrot
2013-08-03
Replacing an association list by a map in globalizing environment.
ppedrot
2013-06-30
Using functors to reduce the boilerplate used in registering
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
