Commit 998b8484 authored by Ralf Jung's avatar Ralf Jung
Browse files

perf experiment: dont make frame_fractional an instance

parent d2c226e7
...@@ -14,9 +14,10 @@ Global Arguments AsFractional {_} _%I _%I _%Qp. ...@@ -14,9 +14,10 @@ Global Arguments AsFractional {_} _%I _%I _%Qp.
Global Arguments fractional {_ _ _} _ _. Global Arguments fractional {_ _ _} _ _.
Global Hint Mode AsFractional - + - - : typeclass_instances. Global Hint Mode AsFractional - ! - - : typeclass_instances.
(* To make [as_fractional_fractional] a useful instance, we have to (* To make [as_fractional_fractional] a useful instance, we have to
allow [q] to be an evar. *) allow [q] to be an evar. The head of [Φ] will always be a λ so ! is
not a useful mode there. *)
Global Hint Mode AsFractional - - + - : typeclass_instances. Global Hint Mode AsFractional - - + - : typeclass_instances.
Section fractional. Section fractional.
...@@ -178,7 +179,8 @@ Section fractional. ...@@ -178,7 +179,8 @@ Section fractional.
Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r
frame_fractional_hyps_half. frame_fractional_hyps_half.
Global Instance frame_fractional p R r Φ P q RES: (* Not an instance because of performance; you can locally add it if you are willing to pay the cost. *)
Lemma frame_fractional p R r Φ P q RES:
AsFractional R Φ r AsFractional P Φ q AsFractional R Φ r AsFractional P Φ q
FrameFractionalHyps p R Φ RES r q FrameFractionalHyps p R Φ RES r q
Frame p R P RES. (* No explicit priority, as default prio > [frame_here]'s 1. *) Frame p R P RES. (* No explicit priority, as default prio > [frame_here]'s 1. *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment