]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_refiner/nCicUnifHint.mli
0e837a01873d231dbe5c992e294f096c994f489b
[helm.git] / matita / components / ng_refiner / nCicUnifHint.mli
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: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
13
14 type db
15
16 exception HintNotValid
17
18 class type g_status =
19  object
20   method uhint_db: db
21  end
22
23 class virtual status :
24  object ('self)
25   inherit g_status
26   inherit NCic.status
27   method set_uhint_db: db -> 'self
28   method set_unifhint_status: #g_status -> 'self
29  end
30
31 val index_hint: 
32   (#status as 'status) -> NCic.context -> NCic.term -> NCic.term -> int -> 'status
33
34 val add_user_provided_hint :
35   (#status as 'status) -> NCic.term -> int -> 'status
36
37 val look_for_hint:
38     #status ->
39     NCic.metasenv -> NCic.substitution -> NCic.context -> 
40     NCic.term -> NCic.term -> 
41       (NCic.metasenv * 
42         (NCic.term * NCic.term) * (NCic.term * NCic.term) list) list
43
44 val eq_class_of:
45       #status -> NCic.term -> NCic.term list
46
47 val generate_dot_file: #status -> Format.formatter -> unit