From f71d59dacdb151f6e5c48b575a536eccfc6d0d32 Mon Sep 17 00:00:00 2001
From: bertot
Date: Tue, 18 Dec 2001 14:25:32 +0000
Subject: There remained traces of streams with the old syntax.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2316 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/blast.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 104051b2d1..102135e96d 100755
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -112,7 +112,7 @@ let pr_bar () = str "|"
 let rec print_info_script sigma osign pf =
   let {evar_hyps=sign; evar_concl=cl} = pf.goal in
   match pf.ref with
-    | None -> [< >]
+    | None -> (mt ())
     | Some(r,spfl) ->
         pr_rule r ++
            match spfl with
@@ -321,7 +321,7 @@ module MySearch = Explore.Make(MySearchProblem)
 let make_initial_state n gl dblist localdb =
   { MySearchProblem.depth = n;
     MySearchProblem.tacres = tclIDTAC gl;
-    MySearchProblem.last_tactic = [< >];
+    MySearchProblem.last_tactic = (mt ());
     MySearchProblem.dblist = dblist;
     MySearchProblem.localdb = [localdb] }
 
-- 
cgit v1.2.3