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/comDefinition.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'vernac/comDefinition.mli')

diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index af09a83f02..256abed6a1 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Entries
 open Decl_kinds
 open Redexpr
 open Constrexpr
@@ -41,5 +40,5 @@ val interp_definition
   -> red_expr option
   -> constr_expr
   -> constr_expr option
-  -> Evd.side_effects definition_entry *
+  -> Evd.side_effects Proof_global.proof_entry *
      Evd.evar_map * UState.universe_decl * Impargs.manual_implicits
-- 
cgit v1.2.3