diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:35:45 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:35:45 +0000 |
| commit | c1dc67b1e5b4add067571955f5fd5e0f6ab1a3be (patch) | |
| tree | d96bd49af498dfc13c7a90c1e1b4284e6c3d9705 /parsing | |
| parent | 386d36deb6efb755cdd16ad216361e01e0b7662e (diff) | |
New option Default Goal Selector.
Set Default Goal Selector "all" prefixes all tactics with "all:" if no selector
is specified (it is overridden by 1: for instance).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16983 85f007b7-540e-0410-9357-904b9bb8a0f7
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: |