ocaml 3.09 transition

[helm.git] / helm / ocaml / cic_proof_checking / cicRecord.mli

diff --git a/helm/ocaml/cic_proof_checking/cicRecord.mli b/helm/ocaml/cic_proof_checking/cicRecord.mli
index 780d859a8bcae2dfda08f10146c57c305b7e3a92..b966f317ca3a951a1a4125a76a431f4bb7c18527 100644 (file)
--- 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