From 3eb1ae56f9f2ee380e6cc323ab2cbaeb45cdf386 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 6 Dec 2001 01:57:08 +0000
Subject: Amélioration nommage hypothèses NewInduction (et incompatibilités)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2275 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml       | 25 +++++++++++++++++--------
 theories/Arith/Between.v |  4 ++--
 2 files changed, 19 insertions(+), 10 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index dc87c10f2c..90c937dfee 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1144,22 +1144,31 @@ let induct_discharge old_style mind statuslists cname destopt avoid ra gl =
   let tophyp = ref None in
   let n = List.fold_left (fun n b -> if b then n+1 else n) 0 ra in
   let recvarname =
-    if n=1 then 
+(*    if n=1 then *)
       cname
-    else (* To force renumbering if there is only one *)
-      make_ident (string_of_id cname) (Some 1)
+(*    else (* To force renumbering if there is only one *)
+      make_ident (string_of_id cname) (Some 1)*)
   in
   let indhyp = if old_style then "Hrec" else "IH" in
   let hyprecname =
     add_prefix indhyp 
-      (if old_style || atompart_of_id recvarname <> "H" then recvarname
+      (if old_style || atompart_of_id cname <> "H" then cname
        else (snd (Global.lookup_inductive mind)).mind_typename)
   in
   let avoid =
-    if old_style then avoid
-    else (* Forbid to use cname0 and hyprecname0 *)
-      (make_ident (string_of_id cname) (Some 0)) ::
-      (make_ident (string_of_id hyprecname) (Some 0)) :: avoid in
+    if n=1
+      or old_style (* for compatibility *)
+      or n=0
+(*            & atompart_of_id cname <> "H" (* for compatibility *)*)
+    then avoid (* Rem: n=0 if Desctruct *)
+    else (* Forbid to use cname, cname0, hyprecname and hyprecname0 *)
+      let avoid =
+        (make_ident (string_of_id cname) (Some 0)) :: (* here for compat *)
+        (make_ident (string_of_id hyprecname) None) ::
+        (make_ident (string_of_id hyprecname) (Some 0)) :: avoid in
+      if atompart_of_id cname <> "H" then
+        (make_ident (string_of_id cname) None) :: avoid 
+      else avoid in
   let rec peel_tac = function
     | true :: ra' ->
 		 (* For lstatus but _buggy_: if intro_gen renames
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index e6b4446017..1c08cdba37 100755
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -126,8 +126,8 @@ Qed.
 
 Lemma in_int_exists : (k,l,r:nat)(in_int k l r)->(Q r)->(exists k l).
 Proof.
-NewInduction 1; Intros.
-Elim H1; Auto with arith.
+NewDestruct 1; Intros.
+Elim H0; Auto with arith.
 Qed.
 
 Lemma between_or_exists : 
-- 
cgit v1.2.3