better nlet rec boxing

[helm.git] / helm / software / components / library / cicElim.ml

diff --git a/helm/software/components/library/cicElim.ml b/helm/software/components/library/cicElim.ml
index 282383d7853ae344ecbb75e09ca45e9d586202c7..9f3bda42304490f51701271d8f83e54c27aa675c 100644 (file)
--- 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;;