From b707a3012eb219de8b3575c84f9e312b4007e4aa Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 29 Jun 2016 13:13:04 -0700 Subject: Handle fractions in denominators This should deal with #16 / https://github.com/mit-plv/fiat-crypto/pull/16#discussion_r69009776 --- src/Algebra.v | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) (limited to 'src/Algebra.v') diff --git a/src/Algebra.v b/src/Algebra.v index 81d1b102b..c0f3b1fba 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -732,15 +732,10 @@ Ltac set_nonfraction_pieces_on T eq zero opp add sub mul inv div nonzero_tac con | appcontext[div] => lazymatch T with | div ?numerator ?denominator - => let d := fresh "d" in - pose denominator as d; - cut (not (eq d zero)); + => cut (not (eq denominator zero)); [ intro; - set_nonfraction_pieces_on - numerator eq zero opp add sub mul inv div nonzero_tac - ltac:(fun numerator' - => cont (div numerator' d)) - | subst d; nonzero_tac ] + two_arg_recr div numerator denominator + | nonzero_tac ] | opp ?x => one_arg_recr opp x | inv ?x => one_arg_recr inv x | add ?x ?y => two_arg_recr add x y -- cgit v1.2.3