diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-18 18:04:49 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-18 18:04:49 -0400 |
| commit | aad7ad2084db3c8401bb9c9e783dfe3c0cf511ac (patch) | |
| tree | fbf8e830708ebbeb7fd2fa54b7ceed4edcf13d52 /src/Reflection/InterpProofs.v | |
| parent | ad22d3d211bc84dd50cbd2259e5bb0a3fb735e88 (diff) | |
Work around bug #5149 in 8.6 (broken subst, evars)
This is https://coq.inria.fr/bugs/show_bug.cgi?id=5149, [subst] breaks
evars in 8.6 (regression in the past week or two)
Diffstat (limited to 'src/Reflection/InterpProofs.v')
| -rw-r--r-- | src/Reflection/InterpProofs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/InterpProofs.v b/src/Reflection/InterpProofs.v index eb3e617e5..1be32bc31 100644 --- a/src/Reflection/InterpProofs.v +++ b/src/Reflection/InterpProofs.v @@ -64,6 +64,6 @@ Section language. (flatten_binding_list (t := t') base_type_code (SmartVarVar v') v)) : interpf interp_op x = x'. Proof. - eapply interpf_SmartVarVar; subst; eassumption. + subst; eapply interpf_SmartVarVar; eassumption. Qed. End language. |