From 2243c25c79ab19876ad74452c9cecc7dcc88c67c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 9 Apr 2018 01:33:31 +0200
Subject: [ltac] Deprecate nameless fix/cofix.

LTAC's `fix` and `cofix` do require access to the proof object inside
the tactic monad when used without a name. This is a bit inconvenient
as we aim to make the handling of the proof object purely functional.

Alternatives have been discussed in #7196, and it seems that
deprecating the nameless forms may have the best cost/benefit ratio,
so opening this PR for discussion.

See also #6171.
---
 theories/Sorting/Heap.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Sorting')

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].
-- 
cgit v1.2.3