From fac3598255cacd81d345099c6ed8cc31ce9b0fd2 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Fri, 6 Jul 2012 12:39:18 +0000 Subject: [PATCH] Added NotationPt.name_of_obj. --- matitaB/components/content/notationPt.ml | 6 ++++++ 1 file changed, 6 insertions(+) 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 -- 2.39.2