aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/global.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-06-13 13:00:49 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-06-13 13:09:59 +0200
commitb94dcdd6e4bfac485ffaf9e11f8f3a5b0329ffa4 (patch)
treecd24335dab0779f91b6e8b36aaf19a199b092fa1 /library/global.ml
parent8cb6251702b09186ca41c5ce67464b83ccfb3d16 (diff)
Improving tclWITHHOLES which did not see undefined evars up to
restriction, after last fix commit which precisely possibly restricts evars of a term "t" in "apply t in H" without resolving them.
Diffstat (limited to 'library/global.ml')
0 files changed, 0 insertions, 0 deletions