diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/inductiveops.mli | 8 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 4 | ||||
| -rw-r--r-- | pretyping/tacred.mli | 3 |
3 files changed, 11 insertions, 4 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 52af27747e..f361e8b8d4 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -93,10 +93,10 @@ val build_branch_type : env -> bool -> constr -> constructor_summary -> types (** Raise [Not_found] if not given an valid inductive type *) val extract_mrectype : constr -> inductive * constr list -val find_mrectype : env -> evar_map -> constr -> inductive * constr list -val find_rectype : env -> evar_map -> constr -> inductive_type -val find_inductive : env -> evar_map -> constr -> inductive * constr list -val find_coinductive : env -> evar_map -> constr -> inductive * constr list +val find_mrectype : env -> evar_map -> types -> inductive * constr list +val find_rectype : env -> evar_map -> types -> inductive_type +val find_inductive : env -> evar_map -> types -> inductive * constr list +val find_coinductive : env -> evar_map -> types -> inductive * constr list (********************) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 4cf1e2345c..fc35e2d31c 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1003,6 +1003,10 @@ 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 rec find_hnf_rectype env sigma t = + let ind,t = reduce_to_atomic_ind env sigma t in + ind, snd (decompose_app t) + (* Reduce the weak-head redex [beta,iota/fix/cofix[all],cast,zeta,simpl/delta] or raise [NotStepReducible] if not a weak-head redex *) diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index f0f5f66d31..8fd14dccbc 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -99,5 +99,8 @@ val reduce_to_quantified_ref : val reduce_to_atomic_ref : env -> evar_map -> global_reference -> types -> types +val find_hnf_rectype : + env -> evar_map -> types -> inductive * constr list + val contextually : bool -> occurrences * constr_pattern -> (patvar_map -> reduction_function) -> reduction_function |