From 6e847be2a6846ab11996d2774b6bc507a342a626 Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Wed, 7 Sep 2016 10:28:07 +0200 Subject: micromega : more robust generation of proof terms - Assert a purely arihtmetic sub-goal that is proved independently by reflexion. (This reduces the stress on the conversion test) - Does not use 'abstract' anymore (more natural proof-term) - Fix a parsing bug (certain terms in Prop where not recognized) --- plugins/micromega/MExtraction.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/micromega/MExtraction.v') diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index 0a41af454..d28bb8286 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -50,7 +50,7 @@ Extract Constant Rinv => "fun x -> 1 / x". Extraction "micromega.ml" List.map simpl_cone (*map_cone indexes*) - denorm Qpower + denorm Qpower vm_add n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. -- cgit v1.2.3