accomodate the .. extension

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5350 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 14 insertions, 4 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 6282d1860d..ac3f45577e 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -180,7 +180,7 @@ and ct_COMMAND =
   | CT_show_proofs
   | CT_show_script
   | CT_show_tree
-  | CT_solve of ct_INT * ct_TACTIC_COM
+  | CT_solve of ct_INT * ct_TACTIC_COM * ct_DOTDOT_OPT
   | CT_suspend
   | CT_syntax_macro of ct_ID * ct_FORMULA * ct_INT_OPT
   | CT_tactic_definition of ct_TAC_DEF_NE_LIST
@@ -254,6 +254,9 @@ and ct_DESTRUCT_LOCATION =
     CT_conclusion_location
   | CT_discardable_hypothesis
   | CT_hypothesis_location
+and ct_DOTDOT_OPT =
+    CT_coerce_NONE_to_DOTDOT_OPT of ct_NONE
+  | CT_dotdot
 and ct_EQN =
     CT_eqn of ct_MATCH_PATTERN_NE_LIST * ct_FORMULA
 and ct_EQN_LIST =
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index ddf005dbd7..4c3288494e 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -559,10 +559,11 @@ and fCOMMAND = function
 | CT_show_proofs -> fNODE "show_proofs" 0
 | CT_show_script -> fNODE "show_script" 0
 | CT_show_tree -> fNODE "show_tree" 0
-| CT_solve(x1, x2) ->
+| CT_solve(x1, x2, x3) ->
    fINT x1;
    fTACTIC_COM x2;
-   fNODE "solve" 2
+   fDOTDOT_OPT x3;
+   fNODE "solve" 3
 | CT_suspend -> fNODE "suspend" 0
 | CT_syntax_macro(x1, x2, x3) ->
    fID x1;
@@ -708,6 +709,9 @@ and fDESTRUCT_LOCATION = function
 | CT_conclusion_location -> fNODE "conclusion_location" 0
 | CT_discardable_hypothesis -> fNODE "discardable_hypothesis" 0
 | CT_hypothesis_location -> fNODE "hypothesis_location" 0
+and fDOTDOT_OPT = function
+| CT_coerce_NONE_to_DOTDOT_OPT x -> fNONE x
+| CT_dotdot -> fNODE "dotdot" 0
 and fEQN = function
 | CT_eqn(x1, x2) ->
    fMATCH_PATTERN_NE_LIST x1;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index ccc1c8c603..cc06b43f3f 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1566,7 +1566,10 @@ let rec xlate_vernac =
     | VernacAbort None -> CT_abort ctv_ID_OPT_OR_ALL_NONE
     | VernacAbortAll -> CT_abort ctv_ID_OPT_OR_ALL_ALL
     | VernacRestart -> CT_restart
-    | VernacSolve (n, tac, b) -> CT_solve (CT_int n, xlate_tactic tac)
+    | VernacSolve (n, tac, b) -> 
+	CT_solve (CT_int n, xlate_tactic tac,
+		  if b then CT_dotdot
+                  else CT_coerce_NONE_to_DOTDOT_OPT CT_none)
     | VernacFocus nopt -> CT_focus (xlate_int_opt nopt)
     | VernacUnfocus -> CT_unfocus
     |VernacExtend("Extraction", [f;l]) ->