X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicRecord.mli;h=04ee188b52364a4be11df76c9eff5e1405021fe8;hb=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;hp=780d859a8bcae2dfda08f10146c57c305b7e3a92;hpb=53ee2f5095adadffcafb40e436d23dc330d3bd87;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicRecord.mli b/helm/ocaml/cic_proof_checking/cicRecord.mli
index 780d859a8..04ee188b5 100644
--- a/helm/ocaml/cic_proof_checking/cicRecord.mli
+++ b/helm/ocaml/cic_proof_checking/cicRecord.mli
@@ -23,19 +23,5 @@
  * 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 *)    
-val projections_of:
-  record_spec ->
-    (string * string * Cic.term) list
-
-  
+(** projections_of [uri] returns uri * name * term *)    
+val projections_of: UriManager.uri -> (UriManager.uri * string * Cic.term) list