aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface')
-rwxr-xr-xcontrib/interface/blast.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 153d3f6374..ce43da5ded 100755
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -565,7 +565,7 @@ let vire_extvar s =
let blast gls =
let leaf g = {
- status = Incomplete_proof;
+ open_subgoals = 1;
goal = g;
ref = None } in
try (let (sgl,v) as res = !blast_tactic gls in