From 057c39b7af6a909419830e15caeb30859b157be4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 6 Dec 2004 11:19:49 +0000
Subject: Commentaire

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6405 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/inductiveops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 53fb0c4275..c03dab08be 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -189,7 +189,7 @@ let make_arity_signature env dep indf =
     (* We need names everywhere *)
     name_context env
       ((Anonymous,None,build_dependent_inductive env indf)::arsign)
-      (* Costly: would be better to name one for all at definition time *)
+      (* Costly: would be better to name once for all at definition time *)
   else
     (* No need to enforce names *)
     arsign
-- 
cgit v1.2.3