Retour comportement de la version précédente

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@456 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 7 deletions

diff --git a/tactics/elim.ml b/tactics/elim.ml
index 6bc3a4b123..dc89f475e6 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -78,18 +78,23 @@ let rec general_decompose recognizer c gl =
          (onLastHyp (general_decompose_clause recognizer)));
       (exact c)]) gl
 
+let up_to_delta = ref false
+
 let head_in gls indl t =
   try
-    let ity = fst (find_mrectype (pf_env gls) (project gls) t) in
-    List.mem ity indl
+    let ity,_ =
+      if !up_to_delta
+      then find_mrectype (pf_env gls) (project gls) t
+      else extract_mrectype (pf_env gls) (project gls) t
+    in List.mem ity indl
   with Induc -> false
        
 let inductive_of_ident gls id =
-  try 
-    fst (find_mrectype (pf_env gls) (project gls) (pf_global gls id))
-  with Induc ->
-    errorlabstrm "Decompose" 
-      [< print_id id; 'sTR " is not an inductive type" >]
+  match kind_of_term (pf_global gls id) with
+    | IsMutInd ity -> ity
+    | _ ->
+	errorlabstrm "Decompose"
+	  [< print_id id; 'sTR " is not an inductive type" >]
 
 let decompose_these c l gls =
   let indl = List.map (inductive_of_ident gls) l in