Ajout make_arity_signature

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

2 files changed, 9 insertions, 4 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index c8cbf31a6..6bf4813c2 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -165,15 +165,18 @@ let build_dependent_inductive env ((ind, params) as indf) =
 
 (* builds the arity of an elimination predicate in sort [s] *)
 
-let make_arity env dep indf s =
+let make_arity_signature env dep indf =
   let (arsign,_) = get_arity env indf in
   if dep then
     (* We need names everywhere *)
-    it_mkProd_or_LetIn_name env
-      (mkArrow (build_dependent_inductive env indf) (mkSort s)) arsign
+    name_context env
+      ((Anonymous,None,build_dependent_inductive env indf)::arsign)
+      (* Costly: would be better to name one for all at definition time *)
   else
     (* No need to enforce names *)
-    it_mkProd_or_LetIn (mkSort s) arsign
+    arsign
+
+let make_arity env dep indf s = mkArity (make_arity_signature env dep indf, s)
 
 (* [p] is the predicate and [cs] a constructor summary *)
 let build_branch_type env dep p cs =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index ef72ab7a3..09c81c7d7 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -54,6 +54,8 @@ val get_constructors :
 val get_arity : env -> inductive * constr list -> Sign.arity
 val build_dependent_constructor : constructor_summary -> constr
 val build_dependent_inductive   : env -> inductive * constr list -> constr
+val make_arity_signature :
+  env -> bool -> inductive * constr list -> Sign.rel_context
 val make_arity : env -> bool -> inductive * constr list -> sorts -> types
 val build_branch_type : env -> bool -> constr -> constructor_summary -> types