From 301e9cb85c2ac995d71cb7978ceae78621ec3eee Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 29 Jun 2020 13:39:18 +0200
Subject: [obligations] Remove duplicate progmap_remove.

This is already taken of by `declare_definition`, by consistency with
the mutual case.
---
 vernac/declare.ml | 1 -
 1 file changed, 1 deletion(-)

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 =
-- 
cgit v1.2.3