diff options
| -rw-r--r-- | pretyping/tacred.ml | 18 | ||||
| -rw-r--r-- | pretyping/tacred.mli | 5 |
2 files changed, 23 insertions, 0 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 1e25cc195b..09f552ba15 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -907,3 +907,21 @@ 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 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) + | _ -> + try + if reference_of_constr c = ref + then it_mkProd_or_LetIn t l + else raise Not_found + with Not_found -> + try + let t' = nf_betaiota (one_step_reduce env sigma t) in + elimrec env t' l + with NotStepReducible -> raise Not_found + in + elimrec env t [] diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 9d76b655c7..c97a27f6ad 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -61,6 +61,11 @@ val reduce_to_atomic_ind : env -> evar_map -> types -> inductive * types returns [I] and [t'] or fails with a user error *) val reduce_to_quantified_ind : env -> evar_map -> types -> inductive * types +(* [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form + [t'=(x1:A1)..(xn:An)(ref args)] and raise Not_found if not possible *) +val reduce_to_quantified_ref : + env -> evar_map -> Libnames.global_reference -> types -> types + type red_expr = (constr, evaluable_global_reference) red_expr_gen val contextually : constr occurrences -> reduction_function->reduction_function |