+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id$ *)
+
let ppterm =
ref (fun ~context ~subst ~metasenv ?inside_fix t -> "Please, set a pp callback")
;;
let r2s pp_fix_name r =
try
match r with
- | R.Ref (_,u,R.Ind (_,i)) ->
+ | R.Ref (u,R.Ind (_,i)) ->
(match NCicLibrary.get_obj u with
| _,_,_,_, C.Inductive (_,_,itl,_) ->
let _,name,_,_ = List.nth itl i in name
| _ -> assert false)
- | R.Ref (_,u,R.Con (i,j)) ->
+ | R.Ref (u,R.Con (i,j)) ->
(match NCicLibrary.get_obj u with
| _,_,_,_, C.Inductive (_,_,itl,_) ->
let _,_,_,cl = List.nth itl i in
let _,name,_ = List.nth cl (j-1) in name
| _ -> assert false)
- | R.Ref (_,u,(R.Decl | R.Def )) ->
+ | R.Ref (u,(R.Decl | R.Def _)) ->
(match NCicLibrary.get_obj u with
| _,_,_,_, C.Constant (_,name,_,_,_) -> name
| _ -> assert false)
- | R.Ref (_,u,(R.Fix (i,_)|R.CoFix i)) ->
+ | R.Ref (u,(R.Fix (i,_,_)|R.CoFix i)) ->
(match NCicLibrary.get_obj u with
| _,_,_,_, C.Fixpoint (_,fl,_) ->
if pp_fix_name then