diff options
| author |  Jasper Hugunin <jasperh@cs.washington.edu> | 2018-06-29 17:31:25 -0700 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-07-02 00:30:17 -0400 |
| commit | 6a8f392badaf7b736651d8349a4eaced47fa2d5e (patch) | |
| tree | dcc5dcb9458981ee20c519d696afa1eee21fd5dc | |
| parent | 82d13637b9ebe6b0562200427e0533f10688bbcc (diff) | |
Make all parameters implicit
| -rw-r--r-- | src/Arithmetic/BarrettReduction/RidiculousFish.v | 2 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/Language.v | 5 | ||||
| -rw-r--r-- | src/Experiments/PartialEvaluationWithLetIn.v | 10 | ||||
| -rw-r--r-- | src/Util/GlobalSettings.v | 3 |
4 files changed, 11 insertions, 9 deletions
diff --git a/src/Arithmetic/BarrettReduction/RidiculousFish.v b/src/Arithmetic/BarrettReduction/RidiculousFish.v index e3f00d7a9..908e098b8 100644 --- a/src/Arithmetic/BarrettReduction/RidiculousFish.v +++ b/src/Arithmetic/BarrettReduction/RidiculousFish.v @@ -32,7 +32,7 @@ Definition wrap (bits val : Z) : Z := val mod 2^bits. (** A [word] is a C data type with a specified bit size. *) Inductive word (bits : Z) := -| Word : Z -> word bits. +| Word (v : Z). Definition to_Z {bits : Z} (a : word bits) : Z := match a with Word v => v end. diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v index 0f67d73ec..f839d8949 100644 --- a/src/Experiments/NewPipeline/Language.v +++ b/src/Experiments/NewPipeline/Language.v @@ -72,9 +72,8 @@ Module Compilers. End Reify. Module type. - Inductive type (base_type : Type) := base (t : base_type) | arrow (s d : type base_type). - Global Arguments base {_}. - Global Arguments arrow {_} s d. + Inductive type {base_type : Type} := base (t : base_type) | arrow (s d : type). + Global Arguments type : clear implicits. Fixpoint final_codomain {base_type} (t : type base_type) : base_type := match t with diff --git a/src/Experiments/PartialEvaluationWithLetIn.v b/src/Experiments/PartialEvaluationWithLetIn.v index b7e018673..82a34c528 100644 --- a/src/Experiments/PartialEvaluationWithLetIn.v +++ b/src/Experiments/PartialEvaluationWithLetIn.v @@ -14,9 +14,8 @@ Require Import Crypto.Util.Notations. *) Module type. - Inductive type (base_type : Type) := base (t : base_type) | arrow (s d : type base_type). - Global Arguments base {_}. - Global Arguments arrow {_} s d. + Inductive type {base_type : Type} := base (t : base_type) | arrow (s d : type). + Global Arguments type : clear implicits. Fixpoint for_each_lhs_of_arrow {base_type} (f : type base_type -> Type) (t : type base_type) : Type := match t with @@ -204,8 +203,9 @@ Module ident. | Cast {T} (upper_bound : upperboundT T) : pident (#T -> #T)%ptype . - Inductive wident (pident : ptype -> Type) : type -> Type := - | wrap {T} (idc : pident T) : wident pident (parametric.subst T). + Inductive wident {pident : ptype -> Type} : type -> Type := + | wrap {T} (idc : pident T) : wident (parametric.subst T). + Global Arguments wident : clear implicits. Definition ident := wident pident. Definition pwrap {T} (idc : pident T) : ident _ := @wrap pident T idc. End with_base. diff --git a/src/Util/GlobalSettings.v b/src/Util/GlobalSettings.v index 001799aa3..f8ab4964f 100644 --- a/src/Util/GlobalSettings.v +++ b/src/Util/GlobalSettings.v @@ -5,6 +5,9 @@ => _ end]. *) Global Set Asymmetric Patterns. +(** Enforce uniform parameters *) +Global Set Uniform Inductive Parameters. + (** Consider also: *) (** Judgmental η for records, faster projections *) (** Set Primitive Projections. *) |