(***************************************************************************) (* This is part of aac_tactics, it is distributed under the terms of the *) (* GNU Lesser General Public License version 3 *) (* (see file LICENSE for more details) *) (* *) (* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) (***************************************************************************) (** Definition of the tactics, and corresponding Coq grammar entries.*)