X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicRecord.mli;h=b966f317ca3a951a1a4125a76a431f4bb7c18527;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=780d859a8bcae2dfda08f10146c57c305b7e3a92;hpb=94818c0bb29820bdf276faa8e515b284c8df0c40;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicRecord.mli b/helm/ocaml/cic_proof_checking/cicRecord.mli
index 780d859a8..b966f317c 100644
--- a/helm/ocaml/cic_proof_checking/cicRecord.mli
+++ b/helm/ocaml/cic_proof_checking/cicRecord.mli
@@ -23,19 +23,6 @@
  * http://helm.cs.unibo.it/
  *)
 
-(** [suri] [params] [ty] [fields] *)
-type record_spec = 
-  string * (string * Cic.term) list * Cic.term * (string * Cic.term) list
-
-(** inductive_of_record [record_spec] returns
- *  types * leftno * obj * ugraph *)
-val inductive_of_record: 
-  record_spec ->
-    Cic.inductiveType list * int * Cic.obj * CicUniv.universe_graph
-    
-(** projections_of [record_spec] returns suri * name * term *)    
+(** projections_of [uri] returns uri * name * term *)    
 val projections_of:
-  record_spec ->
-    (string * string * Cic.term) list
-
-  
+ UriManager.uri -> string list -> (UriManager.uri * string * Cic.term) list