aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofview.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proofview.mli')
-rw-r--r--proofs/proofview.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 45a0c9484..50e1d5eb8 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 ***)