From df1a51daed17539599db551073c9013326cd3068 Mon Sep 17 00:00:00 2001
From: Valentin Blot <24938579+vblot@users.noreply.github.com>
Date: Fri, 20 Jul 2018 18:05:22 +0200
Subject: now compiles with standard coq (including 8.6.1 from opam)

---
 src/versions/native/structures.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/versions/native/structures.mli')

diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli
index 057625c..ba095c8 100644
--- a/src/versions/native/structures.mli
+++ b/src/versions/native/structures.mli
@@ -38,3 +38,4 @@ module Micromega_plugin_Certificate = Certificate
 module Micromega_plugin_Coq_micromega = Coq_micromega
 module Micromega_plugin_Micromega = Micromega
 module Micromega_plugin_Mutils = Mutils
+type tactic = Proof_type.tactic
-- 
cgit