From 3ed367dcc232e01224c133f9a810c5126cdb0f48 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 17 Oct 2017 22:23:11 -0400 Subject: Allow instantiating type arguments without reducing matches --- src/Util/CPSUtil.v | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'src/Util/CPSUtil.v') diff --git a/src/Util/CPSUtil.v b/src/Util/CPSUtil.v index 5f5532d46..df7d3a934 100644 --- a/src/Util/CPSUtil.v +++ b/src/Util/CPSUtil.v @@ -91,11 +91,11 @@ Proof. Qed. Hint Rewrite @flat_map_cps_correct using (intros; autorewrite with uncps; auto): uncps. -Fixpoint from_list_default'_cps {A} (d y:A) n xs: - forall {T}, (Tuple.tuple' A n -> T) -> T:= - match n as n0 return (forall {T}, (Tuple.tuple' A n0 ->T) ->T) with - | O => fun T f => f y - | S n' => fun T f => +Fixpoint from_list_default'_cps {A} (d y:A) n xs {T}: + (Tuple.tuple' A n -> T) -> T:= + match n as n0 return ((Tuple.tuple' A n0 ->T) ->T) with + | O => fun f => f y + | S n' => fun f => match xs with | nil => from_list_default'_cps d d n' nil (fun r => f (r, y)) | x :: xs' => from_list_default'_cps d x n' xs' (fun r => f (r, y)) @@ -107,11 +107,11 @@ Proof. induction n as [|? IHn]; intros; simpl; [reflexivity|]. break_match; subst; apply IHn. Qed. -Definition from_list_default_cps {A} (d:A) n (xs:list A) : - forall {T}, (Tuple.tuple A n -> T) -> T:= - match n as n0 return (forall {T}, (Tuple.tuple A n0 ->T) ->T) with - | O => fun T f => f tt - | S n' => fun T f => +Definition from_list_default_cps {A} (d:A) n (xs:list A) {T} : + (Tuple.tuple A n -> T) -> T:= + match n as n0 return ((Tuple.tuple A n0 ->T) ->T) with + | O => fun f => f tt + | S n' => fun f => match xs with | nil => from_list_default'_cps d d n' nil f | x :: xs' => from_list_default'_cps d x n' xs' f -- cgit v1.2.3