COMMITED BYTECODE COMPILER

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 17 insertions, 1 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index dbf7bc58e0..5f9f907f52 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -511,6 +511,19 @@ let build_inductive env env_ar record finite inds recargs cst =
     (* Elimination sorts *)
     let isunit = isunit && ntypes = 1 && (not (is_recursive recargs.(0))) in
     let kelim = allowed_sorts env issmall isunit ar_sort in
+    let nconst, nblock = ref 0, ref 0 in 
+    let transf num =
+      let arity = List.length (dest_subterms recarg).(num) in
+      if arity = 0 then 
+	let p  = (!nconst, 0) in
+	incr nconst; p
+      else 
+	let p = (!nblock + 1, arity) in
+	incr nblock; p
+     (* les tag des constructeur constant commence a 0,
+	les tag des constructeur non constant a 1 (0 => accumulator) *)
+    in 
+    let rtbl = Array.init (List.length cnames) transf in
     (* Build the inductive packet *)
     { mind_typename = id;
       mind_nparams = nparamargs;
@@ -523,7 +536,10 @@ let build_inductive env env_ar record finite inds recargs cst =
       mind_consnames = Array.of_list cnames;
       mind_user_lc = lc;
       mind_nf_lc = nf_lc;
-      mind_recargs = recarg;
+      mind_recargs = recarg;    
+      mind_nb_constant = !nconst;
+      mind_nb_args = !nblock;
+      mind_reloc_tbl = rtbl;
     } in
   let packets = array_map2 build_one_packet inds recargs in
   (* Build the mutual inductive *)