diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 502b6b8ea..30c88a11c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -147,8 +147,7 @@ GEXTEND Gram | tac = Tactic.tactic; use_dft_tac = [ "." -> false | "..." -> true ] -> (fun g -> - (* arnaud: attention à choisir le bon défaut. *) - let g = Option.default (SelectNth 1) g in + let g = Option.default (Proof_global.get_default_goal_selector ()) g in VernacSolve(g,tac,use_dft_tac)) ] ] ; located_vernac: |