Plot pgm s works again

coq-community · Mar 8, 2011 · 2814d52 · 2814d52
1 parent 940606d
commit 2814d52
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 3 deletions.
diff --git a/dump/dump.ml b/dump/dump.ml
@@ -15,7 +15,7 @@ open Namegen
 open Recordops
 open Tacmach
 open Coqlib
-open Rawterm
+open Glob_term
 open Util
 open Evd
 open Extend

diff --git a/examples/Circle.v b/examples/Circle.v
@@ -107,10 +107,8 @@ Notation "░ a" := (Vcons bool false _ a) (at level 0, right associativity, onl
 
 Definition Circle:=Eval vm_compute in  (PlotPath 0 7 star (-(1)) 1 star (-(1)) 1 star 40 40 CirclePath).
 Add ML Path "dump".
-(* Needs fixing:
 Declare ML Module "dump".
 Dump Circle.
-*)
 (* Now have a look at plot.pgm *)
 End PlotCirclePath.