aboutsummaryrefslogtreecommitdiff
path: root/plugins/decl_mode
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/decl_mode')
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 7a92c995c9..0236c30958 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -132,7 +132,6 @@ let daimon_tac gls =
let daimon _ pftree =
set_daimon_flag ();
{pftree with
- open_subgoals=0;
ref=Some (Daimon,[])}
let daimon_subtree =