aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/obligations.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/obligations.ml')
-rw-r--r--vernac/obligations.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 181068089..58e4b00fc 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -1185,7 +1185,6 @@ let init_program () =
Coqlib.check_required_library ["Coq";"Init";"Specif"];
Coqlib.check_required_library ["Coq";"Program";"Tactics"]
-
let set_program_mode c =
if c then
if !Flags.program_mode then ()