From 75de485c233dd7bbb6301b49e6702eee205977fb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 25 Jun 2019 12:00:02 +0200
Subject: 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.
---
 tactics/declare.ml | 14 ++++----------
 1 file 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)
-- 
cgit v1.2.3