diff options
| -rw-r--r-- | tactics/Refine.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/Refine.v b/tactics/Refine.v index 33d6d9cab..fe421497f 100644 --- a/tactics/Refine.v +++ b/tactics/Refine.v @@ -7,4 +7,4 @@ Grammar tactic simple_tactic: ast := tcc [ "Refine" castedopenconstrarg($c) ] -> [(Tcc $c)]. Syntax tactic level 0: - tcc [(Tcc $C)] -> ["Refine " $C]. + tcc [ (Refine $C) ] -> ["Refine " $C]. |