Added NotationPt.name_of_obj.

diff --git a/matitaB/components/content/notationPt.ml b/matitaB/components/content/notationPt.ml
index 4804208f0657e6a8c54397ac1e7e0591355159da..7cdb86c80b2afe99c2678af993a7038c5a0d6f84 100644 (file)
--- a/matitaB/components/content/notationPt.ml
+++ b/matitaB/components/content/notationPt.ml
@@ -194,6 +194,12 @@ type 'term obj =
   | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list
       (** left parameters, name, type, fields *)
 
+let name_of_obj = function
+  | Theorem (_,n,_,_,_) | Record (_,n,_,_)
+  | Inductive (_,(n,_,_,_)::_) -> n
+  | _ -> (* empty inductive block *) assert false
+;;
+ 
 let map_variable f (t,u) = f t, HExtlib.map_option f u ;;
 
 let map_pattern f = function