diff options
Diffstat (limited to 'plugins/micromega/Lia.v')
| -rw-r--r-- | plugins/micromega/Lia.v | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v index 3e58e81a..47b6f7c7 100644 --- a/plugins/micromega/Lia.v +++ b/plugins/micromega/Lia.v @@ -8,7 +8,7 @@ (* *) (* Micromega: A reflexive tactic using the Positivstellensatz *) (* *) -(* Frédéric Besson (Irisa/Inria) 2013 *) +(* Frédéric Besson (Irisa/Inria) 2013-2016 *) (* *) (************************************************************************) @@ -16,27 +16,27 @@ Require Import ZMicromega. Require Import ZArith. Require Import RingMicromega. Require Import VarMap. -Require Tauto. +Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". + Ltac preprocess := zify ; unfold Z.succ in * ; unfold Z.pred in *. -Ltac lia := - preprocess; - xlia ; - abstract ( - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)). - -Ltac nia := - preprocess; - xnlia ; - abstract ( - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)). +Ltac zchange := + intros __wit __varmap __ff ; + change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; + apply (ZTautoChecker_sound __ff __wit). + +Ltac zchecker_no_abstract := zchange ; vm_compute ; reflexivity. + +Ltac zchecker_abstract := zchange ; vm_cast_no_check (eq_refl true). + +Ltac zchecker := zchecker_no_abstract. + +Ltac lia := preprocess; xlia zchecker. + +Ltac nia := preprocess; xnlia zchecker. (* Local Variables: *) |