diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-12-03 14:54:06 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-12-03 14:54:06 -0500 |
| commit | 726a3345d37f9e45c9ab660cb73334f18a88cb77 (patch) | |
| tree | 3b4c573575d8c1531ba3ca267a711a599bcd79a3 /src/Reflection | |
| parent | 3e89f6cf8818b09f655323349cec5733bba84f80 (diff) | |
Fewer autogenerated names
Diffstat (limited to 'src/Reflection')
| -rw-r--r-- | src/Reflection/Conversion.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Reflection/Conversion.v b/src/Reflection/Conversion.v index 14dfc5633..b1add2222 100644 --- a/src/Reflection/Conversion.v +++ b/src/Reflection/Conversion.v @@ -59,7 +59,7 @@ Section language. | _ => apply functional_extensionality; intro end. clear e IHe H. - revert dependent e0; revert dependent tC; revert dependent x; induction tx; simpl; [ reflexivity | ]; intros. + revert dependent tC; induction tx; simpl; [ reflexivity | ]; intros. destruct x as [x0 x1]; simpl in *. lazymatch goal with | [ |- ?e0 (?x0', ?x1')%core = _ ] @@ -102,7 +102,7 @@ Section language. end. clear H IHe. generalize (interpf interp_op e); intro x; clear e. - revert dependent e0; revert dependent tC; revert dependent x; induction tx; simpl; + revert dependent tC; induction tx; simpl; [ intros; rewrite_hyp ?*; reflexivity | ]; intros. destruct x as [x0 x1]; simpl in *. lazymatch goal with |