tactics/Refine.v


1
2
3
4
5
6
7
8
9
10


(* $Id$ *)

Declare ML Module "refine".

Grammar tactic simple_tactic: ast :=
  tcc [ "Refine" castedopenconstrarg($c) ] -> [(Tcc $c)].

Syntax tactic level 0:
  tcc [ (Refine $C) ] -> ["Refine " $C].