aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-04-26 14:45:45 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-04-26 14:53:00 +0200
commit10a6452c6bbf618428591d9c40aed945f7fe92b3 (patch)
tree8b573d316c61ed052f4084f20689740409783f62 /tools
parent83c3ee8659f1cee68909570fbf581a0e03233af7 (diff)
Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions