aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/MExtraction.v
blob: 352e422cf7808589372e95958b3d5870de70a0ef (plain)
1
2
3
4
5
6
7
8
9
10
11
12
Require Import micromega.MExtraction.
Require Import RingMicromega.
Require Import QArith.
Require Import VarMap.
Require Import ZMicromega.
Require Import QMicromega.
Require Import RMicromega.

Recursive Extraction
  List.map RingMicromega.simpl_cone (*map_cone  indexes*)
  denorm Qpower vm_add
  n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.