diff options
| -rw-r--r-- | parsing/g_constrnew.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index bf4c3372ef..3df5253e6f 100644 --- a/parsing/g_constrnew.ml4 +++ b/parsing/g_constrnew.ml4 @@ -181,7 +181,7 @@ GEXTEND Gram [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args) | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) ] | "9" - [ ".."; ".."; c = operconstr LEVEL "0"; ".."; ".." -> + [ ".."; c = operconstr LEVEL "0"; ".." -> CAppExpl (loc,(None,Ident (loc,Topconstr.ldots_var)),[c]) ] | "1" LEFTA [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 75222eaa43..2f6b6961c0 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -64,7 +64,7 @@ GEXTEND Gram subgoal_command: [ [ c = check_command; "." -> c | tac = Tactic.tactic; - use_dft_tac = [ "." -> false | ".."; "." -> true ] -> + use_dft_tac = [ "." -> false | "..." -> true ] -> (fun g -> let g = match g with Some gl -> gl | _ -> 1 in VernacSolve(g,tac,use_dft_tac)) ] ] |