diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-18 23:56:06 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-18 23:56:06 +0000 |
| commit | dadfbd96378d4c1b794ffc341bd10cc4d63b225d (patch) | |
| tree | 7ff1c2d295f7ff831302b92de6f00f686d0c9f3b /pretyping | |
| parent | 5536b6d56226c4e53bbd6c5ae9a2c419c6f08874 (diff) | |
Granted legitimate wish #2607 (not exposing crude fixpoint body of
unfolded fixpoints when calling destruct). However, this might break
compatibility.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14823 85f007b7-540e-0410-9357-904b9bb8a0f7
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 52af27747..f361e8b8d 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 4cf1e2345..fc35e2d31 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 f0f5f66d3..8fd14dccb 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 |