From 6a5dcbbfea1af0308a4d49e7c5bcea26d74a739d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 31 May 2019 13:09:23 +0200
Subject: Remove Show Script (deprecated in 8.10)

---
 plugins/funind/recdef.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 216be3797b..de1b592337 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1489,8 +1489,6 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
 	       }
 	  )
        )) pstate in
-     (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
-(*      Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
     let _ = Flags.silently (fun () -> Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None) () in
     ()
 (*      Pp.msgnl (fun _ _ -> str "eqn finished"); *)
-- 
cgit v1.2.3