diff options
| author | Maxime Dénès | 2018-04-16 09:09:44 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-04-16 09:09:44 +0200 |
| commit | 8fdfbdbcb4156571a43db7445dea6cd6cec58a53 (patch) | |
| tree | c14e2d109112f1fef9cf19b293ddd275ad79cbfe /theories/Sorting | |
| parent | ea08600edd8796bc8d2782a1750c628c2f64f3d6 (diff) | |
| parent | 2243c25c79ab19876ad74452c9cecc7dcc88c67c (diff) | |
Merge PR #7200: [ltac] Deprecate nameless fix/cofix.
Diffstat (limited to 'theories/Sorting')
| -rw-r--r-- | theories/Sorting/Heap.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index d9e5ad676e..2ef162be4e 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -148,10 +148,10 @@ Section defs. forall l1:list A, Sorted leA l1 -> forall l2:list A, Sorted leA l2 -> merge_lem l1 l2. Proof. - fix 1; intros; destruct l1. + fix merge 1; intros; destruct l1. apply merge_exist with l2; auto with datatypes. rename l1 into l. - revert l2 H0. fix 1. intros. + revert l2 H0. fix merge0 1. intros. destruct l2 as [|a0 l0]. apply merge_exist with (a :: l); simpl; auto with datatypes. induction (leA_dec a a0) as [Hle|Hle]. |