diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-01 20:34:54 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-01 20:34:54 -0500 |
| commit | 2cda4bb32d639c0462e1a0c4efa7ab9f101be670 (patch) | |
| tree | eb3da139d5ba7d08b1a7661b433a6f43c2e466ed /src/Reflection/TypeInversion.v | |
| parent | 47140a68247234d6cf7d761bf6dcf342e85dfb8d (diff) | |
Fix lazymatch ordering
Diffstat (limited to 'src/Reflection/TypeInversion.v')
| -rw-r--r-- | src/Reflection/TypeInversion.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/Reflection/TypeInversion.v b/src/Reflection/TypeInversion.v index f7f3e9929..efc0d0c5a 100644 --- a/src/Reflection/TypeInversion.v +++ b/src/Reflection/TypeInversion.v @@ -73,11 +73,6 @@ Ltac preinvert_one_type e := move e at top; revert dependent T; refine (preinvert_Tbase P _ _) - | ?P (Prod ?A ?B) - => is_var A; is_var B; - move e at top; revert dependent A; intros A e; - move e at top; revert dependent B; revert A; - refine (preinvert_Prod P _ _) | ?P (Prod (Tbase ?A) (Tbase ?B)) => is_var A; is_var B; move e at top; revert dependent A; intros A e; @@ -96,6 +91,11 @@ Ltac preinvert_one_type e := move e at top; revert dependent C; intros C e; move e at top; revert dependent D; revert A B C; refine (preinvert_Prod4 P _ _) + | ?P (Prod ?A ?B) + => is_var A; is_var B; + move e at top; revert dependent A; intros A e; + move e at top; revert dependent B; revert A; + refine (preinvert_Prod P _ _) | ?P Unit => revert dependent e; refine (preinvert_Unit P _ _) |