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

5 files changed, 13 insertions, 6 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
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 3801a6fd88..a363c6bbb0 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 3ea3d5fd5b..59d440c312 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.