aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--vernac/declare.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/declare.ml b/vernac/declare.ml
index fa1bf361fb..757f5b21bc 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1171,7 +1171,6 @@ let update_obls ~pm prg obls rem =
match prg'.prg_deps with
| [] ->
let pm, kn = declare_definition ~pm prg' in
- let pm = progmap_remove pm prg' in
pm, Defined kn
| l ->
let progs =