From edfda2501f08f18e24bd2e3eca763eb1c2dec0ea Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 18 Oct 2000 17:51:58 +0000
Subject: Simplifications autour de typed_type (renommé types par analogie avec
 sorts); documentation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@727 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/declarations.mli | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 3a85e7e05f..3be72f3fd1 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -22,7 +22,7 @@ type constant_value = lazy_constant_value ref
 type constant_body = {
   const_kind : path_kind;
   const_body : constant_value option;
-  const_type : typed_type;
+  const_type : types;
   const_hyps : named_context; (* New: younger hyp at top *)
   const_constraints : constraints;
   mutable const_opaque : bool }
@@ -56,10 +56,10 @@ type recarg =
 type one_inductive_body = {
   mind_consnames : identifier array;
   mind_typename : identifier;
-  mind_nf_lc : typed_type array; (* constrs and arity with pre-expanded ccl *)
-  mind_nf_arity : typed_type;
-  mind_user_lc : typed_type array option;
-  mind_user_arity : typed_type option;
+  mind_nf_lc : types array; (* constrs and arity with pre-expanded ccl *)
+  mind_nf_arity : types;
+  mind_user_lc : types array option;
+  mind_user_arity : types option;
   mind_sort : sorts;
   mind_nrealargs : int;
   mind_kelim : sorts list;
@@ -76,8 +76,8 @@ type mutual_inductive_body = {
   mind_nparams : int }
 
 val mind_type_finite : mutual_inductive_body -> int -> bool
-val mind_user_lc : one_inductive_body -> typed_type array
-val mind_user_arity : one_inductive_body -> typed_type
+val mind_user_lc : one_inductive_body -> types array
+val mind_user_arity : one_inductive_body -> types
 val mind_nth_type_packet : mutual_inductive_body -> int -> one_inductive_body
 
 val mind_arities_context : mutual_inductive_body -> rel_declaration list
-- 
cgit v1.2.3