From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Fri, 6 Jul 2012 12:39:18 +0000 (+0000)
Subject: Added NotationPt.name_of_obj.
X-Git-Tag: make_still_working~1618
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fac3598255cacd81d345099c6ed8cc31ce9b0fd2;p=helm.git

Added NotationPt.name_of_obj.
---

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