X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcicElim.ml;h=9f3bda42304490f51701271d8f83e54c27aa675c;hb=38ec119c163b0e6f97a9800933d5b71c065332e8;hp=282383d7853ae344ecbb75e09ca45e9d586202c7;hpb=82f61808091c59aa884eb232b96ee1c655dcb39a;p=helm.git

diff --git a/helm/software/components/library/cicElim.ml b/helm/software/components/library/cicElim.ml
index 282383d78..9f3bda423 100644
--- a/helm/software/components/library/cicElim.ml
+++ b/helm/software/components/library/cicElim.ml
@@ -430,4 +430,32 @@ debug_print (lazy (CicPp.ppterm eliminator_body));
   | _ ->
       failwith (sprintf "not an inductive definition (%s)"
         (UriManager.string_of_uri uri))
+;;
 
+let generate_elimination_principles ~add_obj ~add_coercion uri obj =
+ match obj with
+  | Cic.InductiveDefinition (indTypes,_,_,attrs) ->
+     let _,inductive,_,_ = List.hd indTypes in
+     if not inductive then []
+     else
+      let _,all_eliminators =
+        List.fold_left
+          (fun (i,res) _ ->
+            let elim sort =
+              try Some (elim_of ~sort uri i)
+              with Can_t_eliminate -> None
+            in
+             i+1,
+              HExtlib.filter_map 
+               elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ] @ res
+          ) (0,[]) indTypes
+      in
+      List.fold_left
+        (fun lemmas (uri,obj) -> add_obj uri obj @ uri::lemmas) 
+        [] all_eliminators
+  | _ -> []
+;;
+
+
+let init () = 
+  LibrarySync.add_object_declaration_hook generate_elimination_principles;;