From 8db4a882c70008d0eefbbb90b401612906cc9629 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 22 May 2000 17:12:25 +0000
Subject: Changement nommage des hypothèses

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@461 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/elim.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/tactics/elim.ml b/tactics/elim.ml
index dc89f475e6..a9df949ea1 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -71,21 +71,23 @@ let rec general_decompose_clause recognizer =
 (* Faudrait ajouter un COMPLETE pour que l'hypothèse créée ne reste
    pas si aucune élimination n'est possible *)
 
-let rec general_decompose recognizer c gl = 
+(* Meilleures stratégies mais perte de compatibilité *)
+let up_to_delta = ref false (* true *)
+let tmphyp_name = id_of_string "TmpHyp" (* "H" *)
+
+let general_decompose recognizer c gl = 
   let typc = pf_type_of gl c in  
   (tclTHENS (cut typc) 
-     [(tclTHEN intro 
+     [(tclTHEN (intro_using tmphyp_name)
          (onLastHyp (general_decompose_clause recognizer)));
       (exact c)]) gl
 
-let up_to_delta = ref false
-
 let head_in gls indl t =
   try
     let ity,_ =
       if !up_to_delta
       then find_mrectype (pf_env gls) (project gls) t
-      else extract_mrectype (pf_env gls) (project gls) t
+      else extract_mrectype t
     in List.mem ity indl
   with Induc -> false
        
-- 
cgit v1.2.3