From dadfbd96378d4c1b794ffc341bd10cc4d63b225d Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 18 Dec 2011 23:56:06 +0000
Subject: 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
---
 pretyping/inductiveops.mli | 8 ++++----
 pretyping/tacred.ml        | 4 ++++
 pretyping/tacred.mli       | 3 +++
 3 files changed, 11 insertions(+), 4 deletions(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3