diff options
| author | herbelin | 2004-03-17 10:53:49 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-17 10:53:49 +0000 |
| commit | fe0a1f5e856b702a5e4638e22b748d2d8af475c2 (patch) | |
| tree | 7ba4f7de2771861838517e3016aba5dd582fe2da | |
| parent | b9b09645e2443762b9e686a4b5a061055381e10c (diff) | |
Utilisation de '..' pour la notation concrete des motifs recursifs de filtrage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5517 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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)) ] ] |