- | Ind (sp,i) ->
- (match (string_of_path sp) with
- "Coq.Init.Logic_Type.eqT" -> let t0= args.(0) in
- let t1= args.(1) in
- let t2= args.(2) in
- (match (kind_of_term t0) with
- Const c ->
- (match (string_of_path c) with
- "Coq.Reals.Rdefinitions.R"->
+ | Cic.MutInd (u,i,o) ->
+ (match UriManager.string_of_uri u with
+ "cic:/Coq/Init/Logic_Type/eqT.con" ->
+ let t0= arg1 in
+ let arg1= arg2 in
+ let arg2= List.hd(List.tl (List.tl next)) in
+ (match t0 with
+ Cic.Const (u,boh) ->
+ (match UriManager.string_of_uri u with
+ "cic:/Coq/Reals/Rdefinitions/R.con"->