diff options
| -rw-r--r-- | pretyping/inductiveops.mli | 8 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 4 | ||||
| -rw-r--r-- | pretyping/tacred.mli | 3 | ||||
| -rw-r--r-- | proofs/logic.ml | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 2 |
5 files changed, 13 insertions, 6 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 diff --git a/proofs/logic.ml b/proofs/logic.ml index 3801a6fd8..a363c6bbb 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -451,7 +451,7 @@ and mk_casegoals sigma goal goalacc p c = let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in let indspec = - try find_mrectype env sigma ct + try Tacred.find_hnf_rectype env sigma ct with Not_found -> anomaly "mk_casegoals" in let (lbrty,conclty) = type_case_branches_with_names env indspec p c in diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 3ea3d5fd5..59d440c31 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -511,7 +511,7 @@ pr " solve_eval. destruct x as [ | xh xl ]. simpl. unfold eval. rewrite make_op_S. rewrite nmake_op_S. auto. - fold word in *. + simpl word in xh, xl |- *. unfold to_Z in *. rewrite make_op_WW. unfold eval in *. rewrite nmake_WW. f_equal; auto. |