diff options
author | Jason Gross <jgross@mit.edu> | 2016-10-26 15:16:22 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-10-26 15:16:33 -0400 |
commit | f493947f6296911c58e55b0dd23a158804b222c2 (patch) | |
tree | fa0a722c2f2009b91047de70ee6cff4ca848303d | |
parent | c2a9824de5ccc1721d0f41a1d0f770806b67f631 (diff) |
Fix typos
-rw-r--r-- | src/Algebra.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index 78255f94e..bd746d1b6 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -1264,14 +1264,14 @@ Ltac nsatz_strip_fractions_on inv := Ltac nsatz_strip_fractions := match goal with | [ |- ?eq ?x ?y ] - => let F := constr:(_ : Algebra.field (eq:=eq)) in + => let F := constr:(_ : field (eq:=eq)) in lazymatch type of F with - | Algebra.field (inv:=?inv) => nsatz_strip_fractions_on inv + | field (inv:=?inv) => nsatz_strip_fractions_on inv end | [ H : ?eq ?x ?y |- False ] - => let F := constr:(_ : Algebra.field (eq:=eq)) in + => let F := constr:(_ : field (eq:=eq)) in lazymatch type of F with - | Algebra.field (inv:=?inv) => nsatz_strip_fractions_on inv + | field (inv:=?inv) => nsatz_strip_fractions_on inv end end. @@ -1281,13 +1281,13 @@ Ltac nsatz_aggregate_inequalities := | [ H : ((?R ?x ?zero) -> False)%type |- False ] => apply H; clear H | [ |- ((?R ?x ?zero) -> False)%type ] => intro | [ H : (?eq ?x ?zero -> False)%type |- ?eq ?y ?zero ] - => revert H; apply (proj2 (nonzero_hypothesis_to_goal x y)) + => revert H; apply (proj2 (Ring.nonzero_hypothesis_to_goal x y)) end. Ltac nsatz_goal_to_canonical := try match goal with | [ |- ?eq ?x ?y ] - => apply (move_leftR (eq:=eq)); rewrite <- ring_sub_definition; + => apply (Group.move_leftR (eq:=eq)); rewrite <- ring_sub_definition; lazymatch goal with | [ |- eq _ y ] => fail 0 "should not subtract 0" | _ => idtac |