aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/coqInterface.mli
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2022-04-14 17:04:25 +0200
committerChantal Keller <Chantal.Keller@lri.fr>2022-04-14 17:04:25 +0200
commitf06426e6171aebfb0e84ebc53fc9677896fa2003 (patch)
treec0a5c7e90ef6d42ebe5a2869b7849fbdda244647 /src/trace/coqInterface.mli
parente61a54d7581b42259d726389250e1cb63682d8d8 (diff)
parent93a3e47a7c4865789f8e84f427cd639a19063e08 (diff)
downloadsmtcoq-f06426e6171aebfb0e84ebc53fc9677896fa2003.tar.gz
smtcoq-f06426e6171aebfb0e84ebc53fc9677896fa2003.zip
Merge remote-tracking branch 'origin/coq-8.11' into timeout_verit
Diffstat (limited to 'src/trace/coqInterface.mli')
-rw-r--r--src/trace/coqInterface.mli13
1 files changed, 1 insertions, 12 deletions
diff --git a/src/trace/coqInterface.mli b/src/trace/coqInterface.mli
index 1a82d96..86fdd95 100644
--- a/src/trace/coqInterface.mli
+++ b/src/trace/coqInterface.mli
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* SMTCoq *)
-(* Copyright (C) 2011 - 2021 *)
+(* Copyright (C) 2011 - 2022 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
@@ -59,21 +59,12 @@ type econstr = EConstr.t
val econstr_of_constr : constr -> econstr
-(* Modules *)
-val gen_constant : string list list -> string -> constr lazy_t
-val init_modules : string list list
-
-
(* Int63 *)
-val int63_modules : string list list
val mkInt : int -> constr
-val cint : constr lazy_t
(* PArray *)
-val parray_modules : string list list
val max_array_size : int
-val mkArray : types * constr array -> constr
(* Traces *)
@@ -91,8 +82,6 @@ val mkTrace :
(* Micromega *)
module Micromega_plugin_Micromega = Micromega_plugin.Micromega
module Micromega_plugin_Certificate = Micromega_plugin.Certificate
-
-val micromega_coq_proofTerm : constr lazy_t
val micromega_dump_proof_term : Micromega_plugin_Micromega.zArithProof -> constr