diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-27 13:55:56 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-27 13:55:56 +0000 |
| commit | 8ab38a81abd3df8b94ca133a6a679d2504eb577a (patch) | |
| tree | 2de8907be09ba1d1847aa13b10846859778631f5 /pretyping | |
| parent | 97517251989d238c588e25a351f6e39e98ffadca (diff) | |
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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/tacred.ml | 12 | ||||
| -rw-r--r-- | pretyping/tacred.mli | 3 |
2 files changed, 13 insertions, 2 deletions
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 |