Module Gomega


Declare ML Module "gomega".

Grammar tactic simple_tactic : ast :=

  gomegawith

     [ "Gomega" "with" ne_identarg_list($lc) ] ->

          [ (Gomega ($LIST $lc)) ]

| gomega

     [ "Gomega" ] ->

          [ (Gomega) ].

Grammar tactic simple_tactic : ast :=

  before 

     [ "Before"  ne_identarg_list($lc) ] ->

          [ (Before ($LIST $lc)) ].

Index

This page has been generated by coqdoc