Remove unused functions for side effects.

4 files changed, 4 insertions, 9 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 8d43513f26..390ab5e878 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -330,9 +330,6 @@ let run_tactic env tac pr =
   let proofview = Proofview.reset_future_goals tacticced_proofview in
   { pr with proofview ; shelf ; given_up },status
 
-let emit_side_effects eff pr =
-  {pr with proofview = Proofview.emit_side_effects eff pr.proofview}
-
 (*** Commands ***)
 
 let in_proof p k = Proofview.in_proofview p.proofview k
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 85b5084476..1112a26c6b 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -165,8 +165,6 @@ val no_focused_goal : proof -> bool
    used. In which case it is [false]. *)
 val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> proof*bool
 
-val emit_side_effects : Declareops.side_effects -> proof -> proof
-
 val maximal_unfocus : 'a focus_kind -> proof -> proof
 
 (*** Commands ***)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index d7f79f46fb..e09e04744d 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -167,9 +167,6 @@ let return_constr { solution = defs } c = Evarutil.nf_evar defs c
 
 let partial_proof entry pv = List.map (return_constr pv) (List.map fst entry)
 
-let emit_side_effects eff x =
-  { x with solution = Evd.emit_side_effects eff x.solution }
-
 (* let return { initial=init; solution=defs }  = *)
 (*   let evdref = ref defs in *)
 (*   let nf,subst = Evarutil.e_nf_evars_and_universes evdref in *)
@@ -668,6 +665,10 @@ let tclEVARMAP =
 
 let tclENV = Env.get
 
+
+let emit_side_effects eff x =
+  { x with solution = Evd.emit_side_effects eff x.solution }
+
 let tclEFFECTS eff =
   Proof.bind (Proof.ret ())
     (fun () -> (* The Global.env should be taken at exec time *)
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 45a0c94846..50e1d5eb8a 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -58,7 +58,6 @@ val return : proofview -> Evd.evar_map
 
 val partial_proof : entry -> proofview -> constr list
 val initial_goals : entry -> (constr * types) list
-val emit_side_effects : Declareops.side_effects -> proofview -> proofview
 
 (*** Focusing operations ***)