X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicElim.ml;h=e47b48d5d7e05a2ef793c3e8f4578a55bfa08f2f;hb=c0f566c371cefef7666a6d68dd1b6c38ca6918ce;hp=d87d7eb4fdd991654f79fc035596b52a2c843c6e;hpb=ea71e96f90757766465abbdd22aec34d095dbf1d;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml
index d87d7eb4f..e47b48d5d 100644
--- a/helm/ocaml/cic_proof_checking/cicElim.ml
+++ b/helm/ocaml/cic_proof_checking/cicElim.ml
@@ -28,6 +28,8 @@ open Printf
 exception Elim_failure of string
 exception Can_t_eliminate
 
+let debug_print = fun _ -> ()
+
 let fresh_binder =
   let counter = ref ~-1 in
   function
@@ -193,12 +195,6 @@ function
       Cic.Lambda (fresh_binder true,
         CicSubstitution.lift_from (rightno + 1) liftno indty, case)
 
-let string_of_sort = function
-  | Cic.Prop -> "Prop"
-  | Cic.CProp -> "CProp"
-  | Cic.Set -> "Set"
-  | Cic.Type _ -> "Type"
-
 let rec branch (uri, typeno) insource paramsno t fix head args =
   match t with
   | Cic.MutInd (uri', typeno', []) when
@@ -249,7 +245,7 @@ let branch (uri, typeno) insource liftno paramsno t fix head args =
 let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
   let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
   match obj with
-  | Cic.InductiveDefinition (indTypes, params, leftno) ->
+  | Cic.InductiveDefinition (indTypes, params, leftno, _) ->
       let (name, inductive, ty, constructors) =
         try
           List.nth indTypes typeno
@@ -343,8 +339,8 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
         add_params (fun b s t -> Cic.Lambda (b, s, t)) leftno ty cic
       in
 (*
-prerr_endline (CicPp.ppterm eliminator_type);
-prerr_endline (CicPp.ppterm eliminator_body);
+debug_print (CicPp.ppterm eliminator_type);
+debug_print (CicPp.ppterm eliminator_body);
 *)
       let (computed_type, ugraph) =
         try
@@ -368,6 +364,9 @@ prerr_endline (CicPp.ppterm eliminator_body);
         | _ -> assert false
       in
       let name = UriManager.name_of_uri uri ^ suffix in
-      Cic.Constant (name, Some eliminator_body, eliminator_type, [])
-  | _ -> assert false
+      let obj_attrs = [`Class (`Elim sort); `Generated] in
+      Cic.Constant (name, Some eliminator_body, eliminator_type, [], obj_attrs)
+  | _ ->
+      failwith (sprintf "not an inductive definition (%s)"
+        (UriManager.string_of_uri uri))