diff options
| author |  Frédéric Besson <frederic.besson@inria.fr> | 2015-04-27 17:35:59 +0200 |
|---|---|---|
| committer | Frédéric Besson <frederic.besson@inria.fr> | 2015-04-28 18:52:12 +0200 |
| commit | 72644c7f7b3f0fcc56779acfcfa4bfc9f041ebde (patch) | |
| tree | e7ca6d2bb16047debdbc0232519c99a11d9a8d0d /plugins/micromega/Psatz.v | |
| parent | 148cf78a4d85ec56818a8ff00719a775670950b9 (diff) | |
maintenance micromega plugin
- add a nra tactic (similar to nia) for non-linear real arithmetic tactic
- fix a long-standing bug in the reification code
- port to the new proof-engine
Diffstat (limited to 'plugins/micromega/Psatz.v')
| -rw-r--r-- | plugins/micromega/Psatz.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index 675321d99..31d051cb4 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -96,6 +96,14 @@ Ltac psatzl dom := Ltac lra := first [ psatzl R | psatzl Q ]. +Ltac nra := + unfold Rdiv in * ; + xnra ; + abstract + (intros __wit __varmap __ff ; + change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; + apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity). + (* Local Variables: *) |