]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/grafite_parser/nEstatus.ml
Objects are now used to represent also the tactic status.
[helm.git] / helm / software / components / grafite_parser / nEstatus.ml
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department, University of Bologna, Italy.                     
5     ||I||                                                                
6     ||T||  HELM is free software; you can redistribute it and/or         
7     ||A||  modify it under the terms of the GNU General Public License   
8     \   /  version 2 or (at your option) any later version.      
9      \ /   This software is distributed as is, NO WARRANTY.     
10       V_______________________________________________________________ *)
11
12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
13
14 class type ctstatus =
15  object ('self)
16   inherit LexiconEngine.status
17   inherit NRstatus.dumpable_status
18   method set_estatus: ctstatus -> 'self
19  end
20
21 class status : ctstatus =
22  object (self)
23   inherit LexiconEngine.status
24   inherit NRstatus.dumpable_status
25   method set_estatus o =
26    (self#set_lexicon_engine_status (o :> LexiconEngine.status))
27         #set_dumpable_status       (o :> NRstatus.dumpable_status)
28  end