From 38aa25757957e9e9f879509605f06ada5992ca36 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 3 Apr 2020 01:16:22 -0400
Subject: [tmp] Compat API for CI

Rewriter needs a bit of work as it calls a removed function, but no
big deal.
---
 tactics/declare.mli | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'tactics')

diff --git a/tactics/declare.mli b/tactics/declare.mli
index 25dcc84fc8..1fabf80b2a 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -301,3 +301,14 @@ val get_current_goal_context : Proof.t -> Evd.evar_map * Environ.env
   If there is no pending proof then it returns the current global
   environment and empty evar_map. *)
 val get_current_context : Proof.t -> Evd.evar_map * Environ.env
+
+(** Temporarily re-exported for 3rd party code; don't use  *)
+val build_constant_by_tactic :
+  name:Names.Id.t ->
+  ?opaque:opacity_flag ->
+  uctx:UState.t ->
+  sign:Environ.named_context_val ->
+  poly:bool ->
+  EConstr.types ->
+  unit Proofview.tactic ->
+  Evd.side_effects proof_entry * bool * UState.t
-- 
cgit v1.2.3