diff options
| author | Pierre-Marie Pédrot | 2019-06-25 12:00:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-08 20:47:04 +0200 |
| commit | 75de485c233dd7bbb6301b49e6702eee205977fb (patch) | |
| tree | d5627dfca6f93864945fdfeaad2846ddf30d149c | |
| parent | 3ce18524834bb9ff7a9ea14c3f1659decb63af76 (diff) | |
Further cleanup following the removal of pure opaque definitions.
We can statically enforce that opaque definitions are always impure by
means of typing, leading to quite a few simplifications.
| -rw-r--r-- | tactics/declare.ml | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index a37368550b..7ad86baa8d 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -205,7 +205,7 @@ let cast_proof_entry e = const_entry_inline_code = e.proof_entry_inline_code; } -let cast_opaque_proof_entry (type a) (pure : a Safe_typing.effect_entry) (e : a Proof_global.proof_entry) = +let cast_opaque_proof_entry e = let open Proof_global in let typ = match e.proof_entry_type with | None -> assert false @@ -220,14 +220,8 @@ let cast_opaque_proof_entry (type a) (pure : a Safe_typing.effect_entry) (e : a Id.Set.empty, Id.Set.empty else let ids_typ = global_vars_set env typ in - let pf, env = match pure with - | PureEntry -> - let (pf, _), () = Future.force e.proof_entry_body in - pf, env - | EffectEntry -> - let (pf, _), eff = Future.force e.proof_entry_body in - pf, Safe_typing.push_private_constants env eff - in + let (pf, _), eff = Future.force e.proof_entry_body in + let env = Safe_typing.push_private_constants env eff in let vars = global_vars_set env pf in ids_typ, vars in @@ -269,7 +263,7 @@ let define_constant ~side_effect ~name cd = let map (body, eff) = body, eff.Evd.seff_private in let body = Future.chain de.proof_entry_body map in let de = { de with proof_entry_body = body } in - let de = cast_opaque_proof_entry EffectEntry de in + let de = cast_opaque_proof_entry de in [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de) | ParameterEntry e -> [], ConstantEntry (PureEntry, Entries.ParameterEntry e) |