From 60596e870bcb481673fd3108fc1b6478df5a2621 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Jun 2019 22:37:42 +0200
Subject: Split the function used to declare side-effects from the standard
 one.

This ensures that side-effect declarations come with their body, in prevision
of the decoupling of the Safe_typign API for CEP 40.
---
 tactics/declare.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/declare.mli')

diff --git a/tactics/declare.mli b/tactics/declare.mli
index f4bfdb1547..a6c1374a77 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -78,7 +78,7 @@ val declare_private_constant
   -> ?local:import_status
   -> name:Id.t
   -> kind:Decls.logical_kind
-  -> Evd.side_effects constant_entry
+  -> unit proof_entry
   -> Constant.t * Evd.side_effects
 
 (** Since transparent constants' side effects are globally declared, we
-- 
cgit v1.2.3