diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-28 14:26:08 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-28 14:26:22 -0700 |
| commit | 0829afd3f8ad8619869c42cdea6bb9efd06187eb (patch) | |
| tree | 6b4cfe8bd2eea5e19acc9709c123ffbf8002f1de /src/Util/Tactics.v | |
| parent | 4ab9da1b82913f1ad798bcdacd8801f619ee2fdf (diff) | |
Fix field_algebra in 8.4
Diffstat (limited to 'src/Util/Tactics.v')
| -rw-r--r-- | src/Util/Tactics.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index a911ca48d..abfc2499c 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -246,6 +246,7 @@ Ltac side_conditions_before_to_side_conditions_after tac_in H := | tac_in H'; [ .. | subst HT'; eexact H' ] ]; + instantiate; (* required in 8.4 for the [move] to succeed, because evar dependencies *) [ (* We preserve the order of the hypotheses. We need to do this here, after evars are instantiated, and not above. *) move H after H'; clear H' |