diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-17 13:57:57 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-17 13:57:57 -0500 |
| commit | 02479d3444fa05891bf459eba72be97760edb9c9 (patch) | |
| tree | 0cf4c4add6f08ff533a267eb9770352a6040dc1f /src | |
| parent | bbb8f9847d48b2294cd6868148ad469d1ad1b63a (diff) | |
Make arguments of InterpLinearize more implicit
Diffstat (limited to 'src')
| -rw-r--r-- | src/Compilers/LinearizeInterp.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Compilers/LinearizeInterp.v b/src/Compilers/LinearizeInterp.v index c22fc26a3..160826b70 100644 --- a/src/Compilers/LinearizeInterp.v +++ b/src/Compilers/LinearizeInterp.v @@ -10,10 +10,10 @@ Require Import Crypto.Util.Tactics.SpecializeBy. Local Open Scope ctype_scope. Section language. - Context (base_type_code : Type). - Context (interp_base_type : base_type_code -> Type). - Context (op : flat_type base_type_code -> flat_type base_type_code -> Type). - Context (interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst). + Context {base_type_code : Type} + {interp_base_type : base_type_code -> Type} + {op : flat_type base_type_code -> flat_type base_type_code -> Type} + {interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst}. Local Notation flat_type := (flat_type base_type_code). Local Notation type := (type base_type_code). |