diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/discharge.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 09b10538de..859f00a00f 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -173,10 +173,8 @@ let process_constant osecsp nsecsp oldenv (ids_to_discard,modlist) cb = expmod_constant_value cb.const_opaque oldenv modlist cb.const_body in let typ = expmod_type oldenv modlist cb.const_type in let hyps = map_sign_typ (expmod_type oldenv modlist) cb.const_hyps in - let (body',typ',modl) = - abstract_constant ids_to_discard hyps (body,typ) - in - let mods = (Const osecsp, DO_ABSTRACT(Const nsecsp,modl)) :: modlist in + let (body',typ',modl) = abstract_constant ids_to_discard hyps (body,typ) in + let mods = [ (Const osecsp, DO_ABSTRACT(Const nsecsp,modl)) ] in (body', typ'.body, mods) |