(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) (* This file was automatically generated: do not edit *********************) include "CoRN.ma". (* $Id: Opaque_algebra.v,v 1.1 2004/02/11 10:56:57 lcf Exp $ *) (* Opaque cs_crr. *) (* UNEXPORTED Opaque csg_crr. *) (* UNEXPORTED Opaque cm_crr. *) (* UNEXPORTED Opaque cg_crr. *) (* UNEXPORTED Opaque cr_crr. *) (* UNEXPORTED Opaque cf_crr. *) (* UNEXPORTED Opaque csf_fun. *) (* UNEXPORTED Opaque csbf_fun. *) (* UNEXPORTED Opaque csr_rel. *) (* UNEXPORTED Opaque cs_eq. *) (* UNEXPORTED Opaque cs_neq. *) (* UNEXPORTED Opaque cs_ap. *) (* UNEXPORTED Opaque cm_unit. *) (* UNEXPORTED Opaque csg_op. *) (* UNEXPORTED Opaque cg_inv. *) (* UNEXPORTED Opaque cg_minus. *) (* UNEXPORTED Opaque cr_one. *) (* UNEXPORTED Opaque cr_mult. *) (* UNEXPORTED Opaque nexp_op. *) (* UNEXPORTED Opaque cf_div. *)