Adapt to fixing dropped implicit arguments in Context.

mit-plv · Nov 20, 2020 · ace6ea0 · ace6ea0
1 parent fe324e8
commit ace6ea0
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 9 deletions.
diff --git a/src/Rewriter/Language/IdentifiersLibrary.v b/src/Rewriter/Language/IdentifiersLibrary.v
@@ -247,15 +247,15 @@ Module Compilers.
             Context (all_pattern_idents : list { T : Type & T })
                     (pattern_ident_index : forall t, cident t -> nat)
                     (eta_pattern_ident_cps_gen
-                     : forall {T : forall t, cident t -> Type}
+                     : forall (T : forall t, cident t -> Type)
                               (f : forall t idc, T t idc),
                         { f' : forall t idc, T t idc | forall t idc, f' t idc = f t idc }).
             Context (ident : Set)
                     (all_idents : list ident)
                     (ident_index : ident -> nat)
                     (ident_index_idempotent : forall idc, List.nth_error all_idents (ident_index idc) = Some idc)
                     (eta_ident_cps_gen
-                     : forall {T : ident -> Type}
+                     : forall (T : ident -> Type)
                               (f : forall idc, T idc),
                         { f' : forall idc, T idc | forall idc, f' idc = f idc }).
 
@@ -500,20 +500,20 @@ Module Compilers.
           Context (all_pattern_idents : list { T : Type & T })
                   (pattern_ident_index : forall t, cident t -> nat)
                   (eta_pattern_ident_cps_gen eta_pattern_ident_cps_gen_expand_literal
-                   : forall {T : forall t, cident t -> Type}
+                   : forall (T : forall t, cident t -> Type)
                             (f : forall t idc, T t idc),
                       { f' : forall t idc, T t idc | forall t idc, f' t idc = f t idc }).
           Context (raw_ident : Set)
                   (all_raw_idents : list raw_ident)
                   (raw_ident_index : raw_ident -> nat)
                   (raw_ident_index_idempotent : forall idc, List.nth_error all_raw_idents (raw_ident_index idc) = Some idc)
                   (eta_raw_ident_cps_gen
-                   : forall {T : raw_ident -> Type}
+                   : forall (T : raw_ident -> Type)
                             (f : forall idc, T idc),
                       { f' : forall idc, T idc | forall idc, f' idc = f idc }).
           Context (raw_ident_infos_of : raw_ident -> Raw.ident.ident_infos)
                   (split_raw_ident_gen
-                   : forall {t} (idc : cident t),
+                   : forall t (idc : cident t),
                       { ridc : raw_ident
                                & { args : Raw.ident.ident_args (preinfos (raw_ident_infos_of ridc))
                                  | { pf : _ = _

diff --git a/src/Rewriter/Rewriter/InterpProofs.v b/src/Rewriter/Rewriter/InterpProofs.v
@@ -72,7 +72,7 @@ Module Compilers.
                 {try_make_transport_base_cps : type.try_make_transport_cpsT base}
                 {try_make_transport_base_cps_correct : type.try_make_transport_cps_correctT base}
                 {ident var : type -> Type}
-                (eta_ident_cps : forall {T : type -> Type} {t} (idc : ident t)
+                (eta_ident_cps : forall (T : type -> Type) t (idc : ident t)
                                         (f : forall t', ident t' -> T t'),
                     T t)
                 {pident : ptype -> Type}
@@ -384,7 +384,7 @@ Module Compilers.
                 {ident : type -> Type}
                 {base_interp : base -> Type}
                 {ident_interp : forall t, ident t -> type.interp (base.interp base_interp) t}
-                (eta_ident_cps : forall {T : type -> Type} {t} (idc : ident t)
+                (eta_ident_cps : forall (T : type -> Type) t (idc : ident t)
                                         (f : forall t', ident t' -> T t'),
                     T t)
                 {pident : ptype -> Type}

diff --git a/src/Rewriter/Rewriter/Rewriter.v b/src/Rewriter/Rewriter/Rewriter.v
@@ -442,7 +442,7 @@ Module Compilers.
         Local Notation base_type := (base.type base).
         Local Notation pattern_base_type := (pattern.base.type base).
         Context {ident var : type.type base_type -> Type}
-                (eta_ident_cps : forall {T : type.type base_type -> Type} {t} (idc : ident t)
+                (eta_ident_cps : forall (T : type.type base_type -> Type) t (idc : ident t)
                                         (f : forall t', ident t' -> T t'),
                     T t)
                 {pident : type.type pattern_base_type -> Type}

diff --git a/src/Rewriter/Rewriter/Wf.v b/src/Rewriter/Rewriter/Wf.v
@@ -65,7 +65,7 @@ Module Compilers.
                 {try_make_transport_base_cps : type.try_make_transport_cpsT base}
                 {try_make_transport_base_cps_correct : type.try_make_transport_cps_correctT base}
                 {ident : type -> Type}
-                (eta_ident_cps : forall {T : type -> Type} {t} (idc : ident t)
+                (eta_ident_cps : forall (T : type -> Type) t (idc : ident t)
                                         (f : forall t', ident t' -> T t'),
                     T t)
                 {pident : ptype -> Type}