blob: c0ef9b392d5b5a61819bed66590ee641bbea70bd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Require Import micromega.MExtraction.
Require Import RingMicromega.
Require Import QArith.
Require Import VarMap.
Require Import ZMicromega.
Require Import QMicromega.
Require Import RMicromega.
Recursive Extraction
Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
ZMicromega.cnfZ ZMicromega.Zeval_const ZMicromega.bound_problem_fr QMicromega.cnfQ
List.map simpl_cone (*map_cone indexes*)
denorm Qpower vm_add
normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
|
