From 98dab0b2a6df19b3c179bc5fd1e211d76827a754 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 16 Nov 2020 23:11:26 +0100
Subject: Add an explicit signature to the MakeCache functor in Micromega.

---
 plugins/micromega/coq_micromega.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 542b99075d..d3a851ded1 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -2064,7 +2064,11 @@ module MakeCache (T : sig
   val hash_coeff : int -> coeff -> int
   val eq_prover_option : prover_option -> prover_option -> bool
   val eq_coeff : coeff -> coeff -> bool
-end) =
+end) :
+sig
+  type key = T.prover_option * (T.coeff Mc.pol * Mc.op1) list
+  val memo_opt : (unit -> bool) -> string -> (key -> 'a) -> key -> 'a
+end =
 struct
   module E = struct
     type t = T.prover_option * (T.coeff Mc.pol * Mc.op1) list
-- 
cgit v1.2.3