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.
---
 plugins/ltac/rewrite.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 4c29d73038..f977ba34d2 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1902,7 +1902,7 @@ let declare_projection n instance_id r =
     Declare.definition_entry ~types:typ ~univs term
   in
     ignore(Declare.declare_constant n 
-	   (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
+           (Declare.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
 
 let build_morphism_signature env sigma m =
   let m,ctx = Constrintern.interp_constr env sigma m in
@@ -1979,7 +1979,7 @@ let add_morphism_as_parameter atts m n : unit =
   let uctx, instance = build_morphism_signature env evd m in
   let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
   let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
-      (Entries.ParameterEntry
+      (Declare.ParameterEntry
          (None,(instance,uctx),None),
        Decl_kinds.IsAssumption Decl_kinds.Logical)
   in
-- 
cgit v1.2.3