From 2d9aa9c7f84c3a48c870c354cb1a794e7423db50 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 11 Oct 2000 20:11:01 +0000
Subject: Nouveau type rec_declaration

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@699 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.ml  | 11 +++++++----
 kernel/term.mli |  5 +++--
 2 files changed, 10 insertions(+), 6 deletions(-)

(limited to 'kernel')

diff --git a/kernel/term.ml b/kernel/term.ml
index a450e61b73..b70bb05a07 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -54,8 +54,9 @@ type existential = existential_key * constr array
 type constant = section_path * constr array
 type constructor = constructor_path * constr array
 type inductive = inductive_path * constr array
-type fixpoint = (int array * int) * (constr array * name list * constr array)
-type cofixpoint = int * (constr array * name list * constr array)
+type rec_declaration = constr array * name list * constr array
+type fixpoint = (int array * int) * rec_declaration
+type cofixpoint = int * rec_declaration
 
 type kind_of_term =
   | IsRel          of int
@@ -116,8 +117,9 @@ and existential = existential_key * constr array
 and constant = section_path * constr array
 and constructor = constructor_path * constr array
 and inductive = inductive_path * constr array
-and fixpoint = (int array * int) * (constr array * name list * constr array)
-and cofixpoint = int * (constr array * name list * constr array)
+and rec_declaration = constr array * name list * constr array
+and fixpoint = (int array * int) * rec_declaration
+and cofixpoint = int * rec_declaration
 
 and kind_of_term =
   | IsRel          of int
@@ -288,6 +290,7 @@ type existential = Internal.existential
 type constant = Internal.constant
 type constructor = Internal.constructor
 type inductive = Internal.inductive
+type rec_declaration = Internal.rec_declaration
 type fixpoint = Internal.fixpoint
 type cofixpoint = Internal.cofixpoint
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 66ba16db62..f2a49e838f 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -102,8 +102,9 @@ type existential = int * constr array
 type constant = section_path * constr array
 type constructor = constructor_path * constr array
 type inductive = inductive_path * constr array
-type fixpoint = (int array * int) * (constr array * name list * constr array)
-type cofixpoint = int * (constr array * name list * constr array)
+type rec_declaration = constr array * name list * constr array
+type fixpoint = (int array * int) * rec_declaration
+type cofixpoint = int * rec_declaration
 
 
 type kind_of_term =
-- 
cgit v1.2.3