Extraction for Coq 8.13 (#109)

Extraction is back! Some new features:
* Not only an executable is generated, but the ZChaff and veriT checkers are available through a package called Smtcoq_extr
* The command-line arguments are better handled
* The veriT checker is now the default

1 files changed, 0 insertions, 79 deletions

diff --git a/src/extraction/extrNative.mli b/src/extraction/extrNative.mli
deleted file mode 100644
index 775f187..0000000
--- a/src/extraction/extrNative.mli
+++ /dev/null
@@ -1,79 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2022                                          *)
-(*                                                                        *)
-(*     See file "AUTHORS" for the list of authors                         *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-
-type comparison = Eq | Lt | Gt
-type 'a carry = C0 of 'a | C1 of 'a
-
-(*s Unsigned Int *)
-type uint 
-
-(* Conversion with int *)
-val to_int : uint -> int
-val of_int : int -> uint
-val of_uint : int -> uint
-
-(* Conversion with string *)
-val to_string : uint -> string
-val of_string : string -> uint
-
-(* logical operations *)
-val l_sl : uint -> uint -> uint
-val l_sr : uint -> uint -> uint
-val l_and : uint -> uint -> uint
-val l_or : uint -> uint -> uint
-val l_xor : uint -> uint -> uint
-
-(* arithmetic operations *)
-val add : uint -> uint -> uint
-val sub : uint -> uint -> uint
-val mul : uint -> uint -> uint
-val mulc : uint -> uint -> uint * uint
-val div : uint -> uint -> uint
-val rem : uint -> uint -> uint
-
-val lt : uint -> uint -> bool
-val le : uint -> uint -> bool
-val eq : uint -> uint -> bool
-val compare : uint -> uint -> comparison
-
-val head0 : uint -> uint
-val tail0 : uint -> uint
-
-val addc : uint -> uint -> uint carry
-val addcarryc : uint -> uint -> uint carry
-val subc : uint -> uint -> uint carry
-val subcarryc : uint -> uint -> uint carry
-val diveucl : uint -> uint -> uint * uint
-val diveucl_21 : uint -> uint -> uint -> uint * uint
-val addmuldiv : uint -> uint -> uint -> uint
-
-val foldi_cont :
-  (uint -> ('a -> 'b) -> 'a -> 'b) -> uint -> uint -> ('a -> 'b) -> 'a -> 'b
-val foldi_down_cont :
-  (uint -> ('a -> 'b) -> 'a -> 'b) -> uint -> uint -> ('a -> 'b) -> 'a -> 'b
-val print_uint : uint -> uint
-
-
-(*s Persistant array *)
-
-type 'a parray 
-
-val of_array : 'a array -> 'a parray
-
-val parray_make : uint -> 'a -> 'a parray
-val parray_get : 'a parray -> uint -> 'a
-val parray_default : 'a parray -> 'a
-val parray_length : 'a parray -> uint
-val parray_set : 'a parray -> uint -> 'a -> 'a parray
-val parray_copy : 'a parray -> 'a parray
-val parray_reroot : 'a parray -> 'a parray
-