From ffaf841c89505bfc0d5a898344a5f1c8c5bf724c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 1 Jul 2000 17:38:39 +0000
Subject: Précalcul de la forme canonique des constructeurs et arités pour
 traiter les cas du fichier Ensemble.v sans avoir à renormaliser à chaque fois

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@545 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/declarations.ml | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index a48384389d..510e1f12b2 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -47,8 +47,11 @@ type recarg =
 type one_inductive_body = {
   mind_consnames : identifier array;
   mind_typename : identifier;
-  mind_lc : typed_type array;
-  mind_arity : typed_type;
+  mind_nf_lc : typed_type array;
+  mind_nf_arity : typed_type;
+  (* lc and arity as given by user if not in nf; useful e.g. for Ensemble.v *)
+  mind_user_lc : constr array option;
+  mind_user_arity : constr option;
   mind_sort : sorts;
   mind_nrealargs : int;
   mind_kelim : sorts list;
@@ -66,6 +69,14 @@ type mutual_inductive_body = {
 
 let mind_type_finite mib i = mib.mind_packets.(i).mind_finite
 
+let mind_user_lc mip = match mip.mind_user_lc with
+  | None -> Array.map body_of_type mip.mind_nf_lc
+  | Some lc -> lc
+
+let mind_user_arity mip = match mip.mind_user_arity with
+  | None -> body_of_type mip.mind_nf_arity
+  | Some a -> a
+
 (*s Declaration. *)
 
 type mutual_inductive_entry = {
-- 
cgit v1.2.3