X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent%2FnotationPt.ml;h=7cdb86c80b2afe99c2678af993a7038c5a0d6f84;hb=fac3598255cacd81d345099c6ed8cc31ce9b0fd2;hp=4804208f0657e6a8c54397ac1e7e0591355159da;hpb=a343b8da51ffa5127e82e9452590b1a3f68f64a0;p=helm.git

diff --git a/matitaB/components/content/notationPt.ml b/matitaB/components/content/notationPt.ml
index 4804208f0..7cdb86c80 100644
--- 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