diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 638185682b..d483b1e6aa 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1449,7 +1449,7 @@ let _ = in error msg | None -> ()); - solve_nth n (Tacinterp.vernac_interp tcom); + solve_nth n (Tacinterp.interp tcom); print_subgoals(); (* in case a strict subtree was completed, go back to the top of the prooftree *) |