diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-12-12 18:41:18 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-12-12 18:44:36 -0500 |
| commit | bcccf309cf87b6d9377f020bd11a5103a66b7e29 (patch) | |
| tree | 19d5641ba48632d8fcdb5d27ef18cae3f6aeb50f /src/Experiments/NewPipeline/LanguageWf.v | |
| parent | 2688eef101a504648f627b78485b2b87faa12bd7 (diff) | |
Generalize expr.interp_related
This is needed to handle exprs whose var types are value
Diffstat (limited to 'src/Experiments/NewPipeline/LanguageWf.v')
| -rw-r--r-- | src/Experiments/NewPipeline/LanguageWf.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v index a459df399..3919287d4 100644 --- a/src/Experiments/NewPipeline/LanguageWf.v +++ b/src/Experiments/NewPipeline/LanguageWf.v @@ -586,7 +586,7 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ : expr.interp_related interp_ident e v -> @type.eqv t (expr.interp interp_ident e) v. Proof using Type. - induction e; cbn [expr.interp_related expr.interp type.related]; cbv [respectful LetIn.Let_In]. + cbv [expr.interp_related]; induction e; cbn [expr.interp_related_gen expr.interp type.related]; cbv [respectful LetIn.Let_In]. all: repeat first [ progress intros | assumption | solve [ eauto ] |