From 8ab38a81abd3df8b94ca133a6a679d2504eb577a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 27 Jan 2004 13:55:56 +0000
Subject: Bug (destruct/induction ne savent pas traiter le cas non atomique
 avec paramètres)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5252 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/tacred.ml  | 12 ++++++++++--
 pretyping/tacred.mli |  3 +++
 tactics/tactics.ml   |  2 +-
 3 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index e2bd273c45..ce6764c38d 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -925,11 +925,16 @@ let reduce_to_ind_gen allow_product env sigma t =
 let reduce_to_quantified_ind x = reduce_to_ind_gen true x
 let reduce_to_atomic_ind x = reduce_to_ind_gen false x
 
-let reduce_to_quantified_ref env sigma ref t = 
+let reduce_to_ref_gen allow_product env sigma ref t = 
   let rec elimrec env t l = 
     let c, _ = Reductionops.whd_stack t in
     match kind_of_term c with
-      | Prod (n,ty,t') -> elimrec (push_rel (n,None,t) env) t' ((n,None,ty)::l)
+      | Prod (n,ty,t') ->
+	  if allow_product then
+	    elimrec (push_rel (n,None,t) env) t' ((n,None,ty)::l)
+	  else 
+	     errorlabstrm "Tactics.reduce_to_ref_gen"
+	       (str"Not an induction object of atomic type")
       | _ ->
 	  try 
 	    if reference_of_constr c = ref 
@@ -942,3 +947,6 @@ let reduce_to_quantified_ref env sigma ref t =
           with NotStepReducible -> raise Not_found
   in
   elimrec env t []
+
+let reduce_to_quantified_ref = reduce_to_ref_gen true
+let reduce_to_atomic_ref = reduce_to_ref_gen false
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 32e40d3ac5..258778bada 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -66,6 +66,9 @@ val reduce_to_quantified_ind : env ->  evar_map -> types -> inductive * types
 val reduce_to_quantified_ref :
   env ->  evar_map -> Libnames.global_reference -> types -> types
 
+val reduce_to_atomic_ref :
+  env ->  evar_map -> Libnames.global_reference -> types -> types
+
 type red_expr = (constr, evaluable_global_reference) red_expr_gen
 
 val contextually : bool -> constr occurrences -> reduction_function
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a1d6a0435c..687c5ad07a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1235,7 +1235,7 @@ let atomize_param_of_ind (indref,nparams) hyp0 gl =
       let tmptyp0 = pf_get_hyp_typ gl hyp0 in
       (* If argl <> [], we expect typ0 not to be quantified, in order to
          avoid bound parameters... then we call pf_reduce_to_atomic_ind *)
-      let indtyp = pf_apply reduce_to_quantified_ref gl indref tmptyp0 in
+      let indtyp = pf_apply reduce_to_atomic_ref gl indref tmptyp0 in
       let argl = snd (decompose_app indtyp) in
       let c = List.nth argl (i-1) in
       match kind_of_term c with
-- 
cgit v1.2.3