diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-26 15:51:11 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-26 15:51:18 -0400 |
| commit | 6ae14f2969991c7733c2b0458b0c1d5061762365 (patch) | |
| tree | d707b8d19f9fc9eaade6da355083af44a9c41a13 /src/Algebra.v | |
| parent | 51b0418dd551cb16d099c010b9a1908c3b2beca5 (diff) | |
Handle folded [not] in nsatz_strip_fractions
Diffstat (limited to 'src/Algebra.v')
| -rw-r--r-- | src/Algebra.v | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index e7c7d3028..525974e67 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -1263,18 +1263,19 @@ Ltac generalize_inv inv := Ltac nsatz_strip_fractions_on inv := rewrite_field_div_definition inv; generalize_inv inv; specialize_by_assumption. +Ltac nsatz_strip_fractions_with_eq eq := + let F := constr:(_ : field (eq:=eq)) in + lazymatch type of F with + | field (inv:=?inv) => nsatz_strip_fractions_on inv + end. Ltac nsatz_strip_fractions := match goal with - | [ |- ?eq ?x ?y ] - => let F := constr:(_ : field (eq:=eq)) in - lazymatch type of F with - | field (inv:=?inv) => nsatz_strip_fractions_on inv - end - | [ H : ?eq ?x ?y |- False ] - => let F := constr:(_ : field (eq:=eq)) in - lazymatch type of F with - | field (inv:=?inv) => nsatz_strip_fractions_on inv - end + | [ |- ?eq ?x ?y ] => nsatz_strip_fractions_with_eq eq + | [ |- not (?eq ?x ?y) ] => nsatz_strip_fractions_with_eq eq + | [ |- (?eq ?x ?y -> False)%type ] => nsatz_strip_fractions_with_eq eq + | [ H : ?eq ?x ?y |- _ ] => nsatz_strip_fractions_with_eq eq + | [ H : not (?eq ?x ?y) |- _ ] => nsatz_strip_fractions_with_eq eq + | [ H : (?eq ?x ?y -> False)%type |- _ ] => nsatz_strip_fractions_with_eq eq end. Ltac nsatz_final_inequality_to_goal := |