]> matita.cs.unibo.it Git - helm.git/blob - components/cic_proof_checking/cicUnivUtils.mli
- decompose now runs with no arguments (operates on the whole context)
[helm.git] / components / cic_proof_checking / cicUnivUtils.mli
1 (* Copyright (C) 2000, HELM Team.                                              
2  *                                                                             
3  * This file is part of HELM, an Hypertextual, Electronic                      
4  * Library of Mathematics, developed at the Computer Science                   
5  * Department, University of Bologna, Italy.                                   
6  *                                                                             
7  * HELM is free software; you can redistribute it and/or                       
8  * modify it under the terms of the GNU General Public License                 
9  * as published by the Free Software Foundation; either version 2              
10  * of the License, or (at your option) any later version.                      
11  *                                                                             
12  * HELM is distributed in the hope that it will be useful,                     
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of              
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the               
15  * GNU General Public License for more details.                                
16  *                                                                             
17  * You should have received a copy of the GNU General Public License           
18  * along with HELM; if not, write to the Free Software                         
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,                      
20  * MA  02111-1307, USA.                                                        
21  *                                                                             
22  * For details, see the HELM World-Wide-Web page,                              
23  * http://cs.unibo.it/helm/.                                                   
24  *)
25
26   (** cleans the universe graph for a given object and fills universes with URI.
27   * to be used on qed
28   *)
29 val clean_and_fill:
30   UriManager.uri -> Cic.obj -> CicUniv.universe_graph ->
31     CicUniv.universe_graph * CicUniv.universe list * Cic.obj
32