diff options
| author | Hugo Herbelin | 2020-03-22 12:30:55 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-03 20:33:27 +0200 |
| commit | aa889ee516453af65bd74ffedf8ec3761f97eb43 (patch) | |
| tree | 9dbe0527c1fc7dd34eb8fa9a2462d3a96048baaa /theories/setoid_ring | |
| parent | 9e98c1ebb9472f1c77eb0289bd64e525d58d99de (diff) | |
Avoiding using a fixed introduction name in Ltac code of stdlib.
Diffstat (limited to 'theories/setoid_ring')
| -rw-r--r-- | theories/setoid_ring/Field_tac.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/setoid_ring/Field_tac.v b/theories/setoid_ring/Field_tac.v index 89a5ca6740..15b2618e47 100644 --- a/theories/setoid_ring/Field_tac.v +++ b/theories/setoid_ring/Field_tac.v @@ -215,7 +215,7 @@ Ltac fold_field_cond req := Ltac simpl_PCond FLD := let req := get_FldEq FLD in let lemma := get_CondLemma FLD in - try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock); + try (apply lemma; intros ?lock ?lock_def; vm_compute; rewrite lock_def; clear lock_def lock); protect_fv "field_cond"; fold_field_cond req; try exact I. @@ -223,7 +223,7 @@ Ltac simpl_PCond FLD := Ltac simpl_PCond_BEURK FLD := let req := get_FldEq FLD in let lemma := get_CondLemma FLD in - (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock); + (apply lemma; intros ?lock ?lock_def; vm_compute; rewrite lock_def; clear lock_def lock); protect_fv "field_cond"; fold_field_cond req. |