1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
TODO: transfer this to GitHub issues !
----
Rebuild a demo !
-[2014-01-07]
- utiliser ocamlgraph pour le calcul de le cloture transitive
dans la fonction reduce_graph (cf. mail Julien Narboux)
-[2013-09-12]
- adaptation for OCaml 4.00.1 and Coq 8.4pl1 (April 2013)
(.ml -> .ml4 + change in Declarations types)
- tests are nor working as before : TODO
#-----------------
~~ COQ part :
- dependencies on [Parametric Morphism] are not detected...
Well, this is not really true, but links seems to be in the wrong way
(see tests/Morph.v)
- add an option to limit the recursive search to a given level.
- also use Section to organize the graph.
~~ translation to .dot
~~ other tools
- try to export .dpd to sqlite database and use firefox extension
~~ visalisation
- use ocamlgraph/viewgraph in order to be able to add actions on nodes
- interactive visualisation ?...
~~ General :
#-----------------
~~ Fixed :
[07/08/2009] fixed bug : requests on internal COQ modules don't work...
|
