From 12ea3318943f2a47f45d939aa206acc263a6341d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 9 Oct 2020 19:28:43 +0200
Subject: Generalizing and exporting interp_assumption/interp_definition.

This shall be for Record fields consumption.
---
 vernac/comDefinition.mli | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'vernac/comDefinition.mli')

diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index d95e64a85f..7420235449 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -14,6 +14,17 @@ open Constrexpr
 
 (** {6 Definitions/Let} *)
 
+val interp_definition
+  :  program_mode:bool
+  -> Environ.env
+  -> Evd.evar_map
+  -> Constrintern.internalization_env
+  -> Constrexpr.local_binder_expr list
+  -> red_expr option
+  -> constr_expr
+  -> constr_expr option
+  -> Evd.evar_map * (EConstr.t * EConstr.t option) * Impargs.manual_implicits
+
 val do_definition
   :  ?hook:Declare.Hook.t
   -> name:Id.t
-- 
cgit v1.2.3