1 files changed, 0 insertions, 398 deletions
diff --git a/contrib/micromega/micromega.mli b/contrib/micromega/micromega.mli
deleted file mode 100644
index f94f091e..00000000
--- a/contrib/micromega/micromega.mli
+++ /dev/null
@@ -1,398 +0,0 @@
-type __ = Obj.t
-
-type bool =
-  | True
-  | False
-
-val negb : bool -> bool
-
-type nat =
-  | O
-  | S of nat
-
-type 'a option =
-  | Some of 'a
-  | None
-
-type ('a, 'b) prod =
-  | Pair of 'a * 'b
-
-type comparison =
-  | Eq
-  | Lt
-  | Gt
-
-val compOpp : comparison -> comparison
-
-type sumbool =
-  | Left
-  | Right
-
-type 'a sumor =
-  | Inleft of 'a
-  | Inright
-
-type 'a list =
-  | Nil
-  | Cons of 'a * 'a list
-
-val app : 'a1 list -> 'a1 list -> 'a1 list
-
-val nth : nat -> 'a1 list -> 'a1 -> 'a1
-
-val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
-
-type positive =
-  | XI of positive
-  | XO of positive
-  | XH
-
-val psucc : positive -> positive
-
-val pplus : positive -> positive -> positive
-
-val pplus_carry : positive -> positive -> positive
-
-val p_of_succ_nat : nat -> positive
-
-val pdouble_minus_one : positive -> positive
-
-type positive_mask =
-  | IsNul
-  | IsPos of positive
-  | IsNeg
-
-val pdouble_plus_one_mask : positive_mask -> positive_mask
-
-val pdouble_mask : positive_mask -> positive_mask
-
-val pdouble_minus_two : positive -> positive_mask
-
-val pminus_mask : positive -> positive -> positive_mask
-
-val pminus_mask_carry : positive -> positive -> positive_mask
-
-val pminus : positive -> positive -> positive
-
-val pmult : positive -> positive -> positive
-
-val pcompare : positive -> positive -> comparison -> comparison
-
-type n =
-  | N0
-  | Npos of positive
-
-type z =
-  | Z0
-  | Zpos of positive
-  | Zneg of positive
-
-val zdouble_plus_one : z -> z
-
-val zdouble_minus_one : z -> z
-
-val zdouble : z -> z
-
-val zPminus : positive -> positive -> z
-
-val zplus : z -> z -> z
-
-val zopp : z -> z
-
-val zminus : z -> z -> z
-
-val zmult : z -> z -> z
-
-val zcompare : z -> z -> comparison
-
-val dcompare_inf : comparison -> sumbool sumor
-
-val zcompare_rec : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
-
-val z_gt_dec : z -> z -> sumbool
-
-val zle_bool : z -> z -> bool
-
-val zge_bool : z -> z -> bool
-
-val zgt_bool : z -> z -> bool
-
-val zeq_bool : z -> z -> bool
-
-val n_of_nat : nat -> n
-
-val zdiv_eucl_POS : positive -> z -> (z, z) prod
-
-val zdiv_eucl : z -> z -> (z, z) prod
-
-type 'c pol =
-  | Pc of 'c
-  | Pinj of positive * 'c pol
-  | PX of 'c pol * positive * 'c pol
-
-val p0 : 'a1 -> 'a1 pol
-
-val p1 : 'a1 -> 'a1 pol
-
-val peq : ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> bool
-
-val mkPinj_pred : positive -> 'a1 pol -> 'a1 pol
-
-val mkPX :
-  'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
-
-val mkXi : 'a1 -> 'a1 -> positive -> 'a1 pol
-
-val mkX : 'a1 -> 'a1 -> 'a1 pol
-
-val popp : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol
-
-val paddC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol
-
-val psubC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol
-
-val paddI :
-  ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol ->
-  positive -> 'a1 pol -> 'a1 pol
-
-val psubI :
-  ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) ->
-  'a1 pol -> positive -> 'a1 pol -> 'a1 pol
-
-val paddX :
-  'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol
-  -> positive -> 'a1 pol -> 'a1 pol
-
-val psubX :
-  'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1
-  pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
-
-val padd :
-  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol ->
-  'a1 pol
-
-val psub :
-  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1
-  -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
-
-val pmulC_aux :
-  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1
-  pol
-
-val pmulC :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1
-  -> 'a1 pol
-
-val pmulI :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol ->
-  'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
-
-val pmul :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
-
-type 'c pExpr =
-  | PEc of 'c
-  | PEX of positive
-  | PEadd of 'c pExpr * 'c pExpr
-  | PEsub of 'c pExpr * 'c pExpr
-  | PEmul of 'c pExpr * 'c pExpr
-  | PEopp of 'c pExpr
-  | PEpow of 'c pExpr * n
-
-val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol
-
-val ppow_pos :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 pol
-
-val ppow_N :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol
-
-val norm_aux :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
-
-type 'a bFormula =
-  | TT
-  | FF
-  | X
-  | A of 'a
-  | Cj of 'a bFormula * 'a bFormula
-  | D of 'a bFormula * 'a bFormula
-  | N of 'a bFormula
-  | I of 'a bFormula * 'a bFormula
-
-type 'term' clause = 'term' list
-
-type 'term' cnf = 'term' clause list
-
-val tt : 'a1 cnf
-
-val ff : 'a1 cnf
-
-val or_clause_cnf : 'a1 clause -> 'a1 cnf -> 'a1 cnf
-
-val or_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf
-
-val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf
-
-val xcnf :
-  ('a1 -> 'a2 cnf) -> ('a1 -> 'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 cnf
-
-val cnf_checker : ('a1 list -> 'a2 -> bool) -> 'a1 cnf -> 'a2 list -> bool
-
-val tauto_checker :
-  ('a1 -> 'a2 cnf) -> ('a1 -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1
-  bFormula -> 'a3 list -> bool
-
-type 'c pExprC = 'c pExpr
-
-type 'c polC = 'c pol
-
-type op1 =
-  | Equal
-  | NonEqual
-  | Strict
-  | NonStrict
-
-type 'c nFormula = ('c pExprC, op1) prod
-
-type monoidMember = nat list
-
-type 'c coneMember =
-  | S_In of nat
-  | S_Ideal of 'c pExprC * 'c coneMember
-  | S_Square of 'c pExprC
-  | S_Monoid of monoidMember
-  | S_Mult of 'c coneMember * 'c coneMember
-  | S_Add of 'c coneMember * 'c coneMember
-  | S_Pos of 'c
-  | S_Z
-
-val nformula_times : 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula
-
-val nformula_plus : 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula
-
-val eval_monoid : 'a1 -> 'a1 nFormula list -> monoidMember -> 'a1 pExprC
-
-val eval_cone :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula
-  list -> 'a1 coneMember -> 'a1 nFormula
-
-val normalise_pexpr :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExprC -> 'a1 polC
-
-val check_inconsistent :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1
-  nFormula -> bool
-
-val check_normalised_formulas :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1
-  nFormula list -> 'a1 coneMember -> bool
-
-type op2 =
-  | OpEq
-  | OpNEq
-  | OpLe
-  | OpGe
-  | OpLt
-  | OpGt
-
-type 'c formula = { flhs : 'c pExprC; fop : op2; frhs : 'c pExprC }
-
-val flhs : 'a1 formula -> 'a1 pExprC
-
-val fop : 'a1 formula -> op2
-
-val frhs : 'a1 formula -> 'a1 pExprC
-
-val xnormalise : 'a1 formula -> 'a1 nFormula list
-
-val cnf_normalise : 'a1 formula -> 'a1 nFormula cnf
-
-val xnegate : 'a1 formula -> 'a1 nFormula list
-
-val cnf_negate : 'a1 formula -> 'a1 nFormula cnf
-
-val simpl_expr : 'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pExprC -> 'a1 pExprC
-
-val simpl_cone :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 coneMember
-  -> 'a1 coneMember
-
-type q = { qnum : z; qden : positive }
-
-val qnum : q -> z
-
-val qden : q -> positive
-
-val qplus : q -> q -> q
-
-val qmult : q -> q -> q
-
-val qopp : q -> q
-
-val qminus : q -> q -> q
-
-type 'a t =
-  | Empty
-  | Leaf of 'a
-  | Node of 'a t * 'a * 'a t
-
-val find : 'a1 -> 'a1 t -> positive -> 'a1
-
-type zWitness = z coneMember
-
-val zWeakChecker : z nFormula list -> z coneMember -> bool
-
-val xnormalise0 : z formula -> z nFormula list
-
-val normalise : z formula -> z nFormula cnf
-
-val xnegate0 : z formula -> z nFormula list
-
-val negate : z formula -> z nFormula cnf
-
-val ceiling : z -> z -> z
-
-type proofTerm =
-  | RatProof of zWitness
-  | CutProof of z pExprC * q * zWitness * proofTerm
-  | EnumProof of q * z pExprC * q * zWitness * zWitness * proofTerm list
-
-val makeLb : z pExpr -> q -> z nFormula
-
-val qceiling : q -> z
-
-val makeLbCut : z pExprC -> q -> z nFormula
-
-val neg_nformula : z nFormula -> (z pExpr, op1) prod
-
-val cutChecker :
-  z nFormula list -> z pExpr -> q -> zWitness -> z nFormula option
-
-val zChecker : z nFormula list -> proofTerm -> bool
-
-val zTautoChecker : z formula bFormula -> proofTerm list -> bool
-
-val map_cone : (nat -> nat) -> zWitness -> zWitness
-
-val indexes : zWitness -> nat list
-
-val n_of_Z : z -> n
-
-val qeq_bool : q -> q -> bool
-
-val qle_bool : q -> q -> bool
-
-type qWitness = q coneMember
-
-val qWeakChecker : q nFormula list -> q coneMember -> bool
-
-val qTautoChecker : q formula bFormula -> qWitness list -> bool
-