From cc058a45755800e65a4e0fb6a37e8576f2b608d5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 20 Nov 2001 23:04:37 +0000
Subject: Ajout make_arity_signature

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2219 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/inductiveops.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index c8cbf31a62..6bf4813c2e 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 =
-- 
cgit v1.2.3