tactics/Refine.v


1
2
3
4
5
6
7
8
9
10

(* $Id$ *)

Declare ML Module "refine".

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

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