Big commit and major code clean-up:

[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..04ee188b52364a4be11df76c9eff5e1405021fe8 100644 (file)
--- 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