diff options
| author |  Frédéric Besson <frederic.besson@inria.fr> | 2016-09-07 10:28:07 +0200 |
|---|---|---|
| committer | Frédéric Besson <frederic.besson@inria.fr> | 2016-09-07 10:28:07 +0200 |
| commit | 6e847be2a6846ab11996d2774b6bc507a342a626 (patch) | |
| tree | 18ddfc166371881314a763d63ce9e51216fa98fe /plugins/micromega/Lia.v | |
| parent | 977e91d0aa5cfece962fc82e3fd42402918663c8 (diff) | |
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)
Diffstat (limited to 'plugins/micromega/Lia.v')
| -rw-r--r-- | plugins/micromega/Lia.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v index 6974f8d99..47b6f7c7f 100644 --- a/plugins/micromega/Lia.v +++ b/plugins/micromega/Lia.v @@ -30,13 +30,13 @@ Ltac zchange := Ltac zchecker_no_abstract := zchange ; vm_compute ; reflexivity. -Ltac zchecker_abstract := abstract (zchange ; vm_cast_no_check (eq_refl true)). +Ltac zchecker_abstract := zchange ; vm_cast_no_check (eq_refl true). -Ltac zchecker := zchecker_abstract || zchecker_no_abstract . +Ltac zchecker := zchecker_no_abstract. -Ltac lia := preprocess; xlia ; zchecker. +Ltac lia := preprocess; xlia zchecker. -Ltac nia := preprocess; xnlia ; zchecker. +Ltac nia := preprocess; xnlia zchecker. (* Local Variables: *) |