diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-03-03 23:20:53 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-03-03 23:20:53 +0100 |
| commit | 1b7e788a2bc6c7beb5d2e6971574e3349fd2a1cf (patch) | |
| tree | 1e4f0cccfa2e9302d0765d8f06fcd83f10de0265 /plugins/firstorder/formula.ml | |
| parent | c1a330b28cd1417099183a1cb0a86b6a606b7ae9 (diff) | |
Fix bug #3732: firstorder was using detyping to build existential
instances and forgeting about the evars and universes that could appear
there... dirty hack gone, using the evar map properly and avoiding
needless constructions/deconstructions of terms.
Diffstat (limited to 'plugins/firstorder/formula.ml')
0 files changed, 0 insertions, 0 deletions