aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-04-27 14:46:18 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-04-27 14:46:18 +0200
commitb9c8bb1621e017e029e87bc684255eae775718fc (patch)
tree388f86e2ec0342cca25a9fe68e3170c8fde5360c /tools
parent53fb4203b80da48e2ac9b06803c57e81df702a0a (diff)
parent10a6452c6bbf618428591d9c40aed945f7fe92b3 (diff)
Merge PR #7358: Fix #7356: missing lift when interpreting default instances of evars
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions