diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-06 12:06:33 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-06 12:06:33 -0700 |
| commit | d71bd40dcc6dbea9123c0ca613ac44e2ab9d5422 (patch) | |
| tree | c96de8273a05fcda9e01aae088c8f744fdcfd358 /src | |
| parent | a1c7bd0d0cade0df94f36d0dd34ce775817fb391 (diff) | |
Fix for changes in 8.4/8.5 behavior of [intro] w.r.t. refolding
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/Syntax.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 27cbad90f..03e8b21a0 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -47,10 +47,10 @@ Section language. Proof. induction t; repeat intro; reflexivity. Qed. Global Instance interp_type_gen_rel_pointwise_Symmetric {H : forall t, Symmetric (R t)} : forall t, Symmetric (interp_type_gen_rel_pointwise t). - Proof. induction t; repeat intro; symmetry; eauto. Qed. + Proof. induction t; simpl; repeat intro; symmetry; eauto. Qed. Global Instance interp_type_gen_rel_pointwise_Transitive {H : forall t, Transitive (R t)} : forall t, Transitive (interp_type_gen_rel_pointwise t). - Proof. induction t; repeat intro; etransitivity; eauto. Qed. + Proof. induction t; simpl; repeat intro; etransitivity; eauto. Qed. End rel. End type. Section flat_type. |