From f597952e1b216ca5adf9f782c736f4cfe705ef02 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 16 Jun 2019 19:09:25 +0200
Subject: Duplicate the type of constant entries in Proof_global.

This allows to desynchronize the kernel-facing API from the proof-facing one.
---
 vernac/comProgramFixpoint.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'vernac/comProgramFixpoint.ml')

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 23c98c97f9..6c1c23eacb 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -13,7 +13,6 @@ open CErrors
 open Util
 open Constr
 open Context
-open Entries
 open Vars
 open Declare
 open Names
-- 
cgit v1.2.3