contrib/interface/dad.ml4 had no real need of streams, it should have been

translated into a regular ml files like the others.  This mistake is now
corrected.  The Makefile and dependency files are updated accordingly.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2345 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 2 insertions, 12 deletions

diff --git a/.depend b/.depend
index c92f200882..d83d0f6d6a 100644
--- a/.depend
+++ b/.depend
@@ -2247,7 +2247,6 @@ toplevel/mltop.cmo:
 lib/pp.cmo: 
 contrib/xml/xml.cmo: 
 contrib/xml/xmlcommand.cmo: 
-contrib/interface/dad.cmo: 
 contrib/interface/line_parser.cmo: 
 tools/coq_makefile.cmo: 
 tools/coq-tex.cmo: 
diff --git a/.depend.camlp4 b/.depend.camlp4
index 6064e6a838..94a85c9807 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -18,7 +18,6 @@ toplevel/mltop.ml:
 lib/pp.ml: 
 contrib/xml/xml.ml: 
 contrib/xml/xmlcommand.ml: 
-contrib/interface/dad.ml: 
 contrib/interface/line_parser.ml: 
 tools/coq_makefile.ml: 
 tools/coq-tex.ml: 
diff --git a/Makefile b/Makefile
index 8771465bf8..d6ab60f5ce 100644
--- a/Makefile
+++ b/Makefile
@@ -795,12 +795,6 @@ library/nametab.cmx: library/nametab.ml
 #contrib/xml/xmlcommand.cmx: contrib/xml/xmlcommand.ml4
 #	$(OCAMLOPT_P4O) -c $<
 
-#contrib/interface/dad.cmo: contrib/interface/dad.ml4
-#	$(OCAMLC_P4O) -c $<
-
-#contrib/interface/dad.cmx: contrib/interface/dad.ml4
-#	$(OCAMLOPT_P4O) -c $<
-
 #contrib/interface/line_parser.cmo: contrib/interface/line_parser.ml4
 #	$(OCAMLC_P4O) -c $<
 
@@ -822,7 +816,6 @@ library/nametab.cmx: library/nametab.ml
 ML4FILES += lib/pp.ml4 			\
 	 contrib/xml/xml.ml4		\
 	 contrib/xml/xmlcommand.ml4	\
-	 contrib/interface/dad.ml4	\
 	 contrib/interface/line_parser.ml4	\
 	 tools/coq_makefile.ml4		\
 	 tools/coq-tex.ml4
diff --git a/contrib/interface/dad.ml4 b/contrib/interface/dad.ml
index ce38174044..ceb0f5953f 100644
--- a/contrib/interface/dad.ml4
+++ b/contrib/interface/dad.ml
@@ -253,8 +253,7 @@ vinterp_add "AddDadRule"
             (function () ->
               let pr = match decompose_path (p1, p2) with pr, _, _ -> pr in
               (add_dad_rule name (Ctast.ast_to_ct pat) p1 p2 (List.length pr) pr (Ctast.ast_to_ct com)))
-            | _ -> errorlabstrm "AddDadRule1"
-                    [< str "AddDadRule2">]);
+            | _ -> errorlabstrm "AddDadRule1" (str "AddDadRule2"));
 add_dad_rule "distributivity-inv"
 (Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,3)])]);Node(zz,"META",[Num(zz,2)])]))
 [2; 2]
@@ -355,4 +354,4 @@ vinterp_add "StartDad"
    (function
      | [] ->
        (function () -> start_dad())
-     | _ -> errorlabstrm "StartDad" [< >]);;
+     | _ -> errorlabstrm "StartDad" (mt()));;