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) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 +++ 2 files changed, 13 insertions(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index e2bd273c4..ce6764c38 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 32e40d3ac..258778bad 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 -- cgit v1.2.3