(**************************************************************************) (* ___ *) (* ||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 "Coq.ma". (* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/N.con **************************) inline procedural "cic:/Coq/Num/Params/N.con". (* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/zero.con ***********************) inline procedural "cic:/Coq/Num/Params/zero.con". (* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/one.con ************************) inline procedural "cic:/Coq/Num/Params/one.con". (* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/add.con ************************) inline procedural "cic:/Coq/Num/Params/add.con". (* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/S.con **************************) inline procedural "cic:/Coq/Num/Params/S.con". (* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/lt.con *************************) inline procedural "cic:/Coq/Num/Params/lt.con". (* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/le.con *************************) inline procedural "cic:/Coq/Num/Params/le.con". (* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/gt.con *************************) inline procedural "cic:/Coq/Num/Params/gt.con". (* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/ge.con *************************) inline procedural "cic:/Coq/Num/Params/ge.con".