From: Wilmer Ricciotti 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