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

1 files changed, 2 insertions, 2 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 104051b2d..102135e96 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] }