diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-10-25 13:23:58 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-10-25 13:23:58 -0400 |
| commit | 4b4995ed25721acd64dd786a8db52a7630e5ea32 (patch) | |
| tree | 43e79389538ded786047d1115c1a7570640f8821 /src | |
| parent | 8a3eda8ee4ca1df293ba47802959a4474a117412 (diff) | |
Remove value'_interp_related1
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterWf1.v | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v index d91ec0e69..a05fd7b04 100644 --- a/src/Experiments/NewPipeline/RewriterWf1.v +++ b/src/Experiments/NewPipeline/RewriterWf1.v @@ -1327,7 +1327,7 @@ Module Compilers. then UnderLets.interp ident_interp else (fun x => x)). - Fixpoint value'_interp_related1 + Fixpoint value_interp_related1 {with_lets1 t} : @value' var with_lets1 t -> var t @@ -1340,13 +1340,10 @@ Module Compilers. | type.arrow s d => fun (f1 : value' _ s -> value' _ d) (f2 : var s -> var d) => forall x1 x2, - @value'_interp_related1 _ s x1 x2 - -> @value'_interp_related1 _ d (f1 x1) (f2 x2) + @value_interp_related1 _ s x1 x2 + -> @value_interp_related1 _ d (f1 x1) (f2 x2) end. - Definition value_interp_related1 {t} : @value var t -> var t -> Prop - := value'_interp_related1. - Fixpoint value'_interp_related {with_lets1 with_lets2 t} : @value' var with_lets1 t |