"Let in" in pattern hell, one more iteration

This reverts commit 28bcf05dd876beea8697f6ee47ebf916a8b94cdf.

An other wrong externalize function

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15021 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 31 insertions, 0 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index cd86b1e67c..8e9b469bfa 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -107,6 +107,8 @@ let mis_constr_nargs_env env (kn,i) =
   let recargs = dest_subterms mip.mind_recargs in
   Array.map List.length recargs
 
+(* Arity of constructors excluding local defs *)
+
 let mis_constructor_nargs (indsp,j) =
   let (mib,mip) = Global.lookup_inductive indsp in
   recarg_length mip.mind_recargs j + mib.mind_nparams
@@ -116,6 +118,17 @@ let mis_constructor_nargs_env env ((kn,i),j) =
   let mip = mib.mind_packets.(i) in
   recarg_length mip.mind_recargs j + mib.mind_nparams
 
+(* Arity of constructors with arg and defs *)
+
+let mis_constructor_nhyps (indsp,j) =
+  let (mib,mip) = Global.lookup_inductive indsp in
+   mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt)
+
+let mis_constructor_nhyps_env env ((kn,i),j) =
+  let mib = Environ.lookup_mind kn env in
+  let mip = mib.mind_packets.(i) in
+   mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt)
+
 let constructor_nrealargs env (ind,j) =
   let (_,mip) = Inductive.lookup_mind_specif env ind in
   recarg_length mip.mind_recargs j
@@ -132,6 +145,16 @@ let nconstructors ind =
   let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
   Array.length mip.mind_consnames
 
+let mis_constructor_has_local_defs (indsp,j) =
+  let (mib,mip) = Global.lookup_inductive indsp in
+  mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt)
+  <> recarg_length mip.mind_recargs j + mib.mind_nparams
+
+let inductive_has_local_defs ind =
+  let (mib,mip) = Global.lookup_inductive ind in
+  rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealargs_ctxt
+  <> mib.mind_nparams + mip.mind_nrealargs
+
 (* Length of arity (w/o local defs) *)
 
 let inductive_nparams ind =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 5cf84acd7a..3fb0907dfa 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -74,12 +74,20 @@ val inductive_nparams : inductive -> int
 val mis_constructor_nargs : constructor -> int
 val mis_constructor_nargs_env : env -> constructor -> int
 
+(** @return param + args with letin *)
+val mis_constructor_nhyps : constructor -> int
+val mis_constructor_nhyps_env : env -> constructor -> int
+
 (** @return args without letin *)
 val constructor_nrealargs : env -> constructor -> int
 
 (** @return args with letin *)
 val constructor_nrealhyps : constructor -> int
 
+(** Is there local defs in params or args ? *)
+val mis_constructor_has_local_defs : constructor -> bool
+val inductive_has_local_defs : inductive -> bool
+
 val get_full_arity_sign : env -> inductive -> rel_context
 
 val allowed_sorts : env -> inductive -> sorts_family list