diff options
Diffstat (limited to 'tactics/Refine.v')
| -rw-r--r-- | tactics/Refine.v | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/tactics/Refine.v b/tactics/Refine.v index 4d6c117e3e..72ecf89fe1 100644 --- a/tactics/Refine.v +++ b/tactics/Refine.v @@ -8,10 +8,4 @@ (* $Id$ *) -Declare ML Module "refine". - -Grammar tactic simple_tactic: ast := - tcc [ "Refine" castedopenconstrarg($c) ] -> [(Tcc $c)]. - -Syntax tactic level 0: - tcc [ <<(Tcc $C)>> ] -> ["Refine " $C]. +(* Command declarations are moved to the ML side *) |