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.
---
 vernac/pfedit.ml       | 9 +++++++++
 vernac/proof_global.ml | 7 +++++++
 vernac/vernac.mllib    | 2 ++
 3 files changed, 18 insertions(+)
 create mode 100644 vernac/pfedit.ml
 create mode 100644 vernac/proof_global.ml

(limited to 'vernac')

diff --git a/vernac/pfedit.ml b/vernac/pfedit.ml
new file mode 100644
index 0000000000..d6b9592176
--- /dev/null
+++ b/vernac/pfedit.ml
@@ -0,0 +1,9 @@
+(* Compat API / *)
+let get_current_context = Declare.get_current_context
+let solve = Proof.solve
+let by = Declare.by
+let refine_by_tactic = Proof.refine_by_tactic
+
+(* We don't want to export this anymore, but we do for now *)
+let build_by_tactic = Declare.build_by_tactic
+let build_constant_by_tactic = Declare.build_constant_by_tactic
diff --git a/vernac/proof_global.ml b/vernac/proof_global.ml
new file mode 100644
index 0000000000..b6c07042e2
--- /dev/null
+++ b/vernac/proof_global.ml
@@ -0,0 +1,7 @@
+(* compatibility module; can be removed once we agree on the API *)
+
+type t = Declare.Proof.t
+let map_proof = Declare.Proof.map_proof
+let get_proof = Declare.Proof.get_proof
+
+type opacity_flag = Declare.opacity_flag = Opaque | Transparent
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 5a2bdb43d4..b7728fe699 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -44,3 +44,5 @@ ComArguments
 Vernacentries
 Vernacstate
 Vernacinterp
+Proof_global
+Pfedit
-- 
cgit v1.2.3