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 /src/Experiments/PartialEvaluationWithLetIn.v | |
| parent | 82d13637b9ebe6b0562200427e0533f10688bbcc (diff) | |
Make all parameters implicit
Diffstat (limited to 'src/Experiments/PartialEvaluationWithLetIn.v')
| -rw-r--r-- | src/Experiments/PartialEvaluationWithLetIn.v | 10 |
1 files changed, 5 insertions, 5 deletions
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. |