diff options
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 6 |
1 files changed, 5 insertions, 1 deletions
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 |