diff options
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 ] |