include "Coq.ma".
-(*#**********************************************************************)
-
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-
-(* \VV/ *************************************************************)
-
-(* // * This file is distributed under the terms of the *)
-
-(* * GNU Lesser General Public License Version 2.1 *)
-
-(*#**********************************************************************)
-
-(*i $Id: Definitions.v,v 1.3 2002/02/14 14:39:02 filliatr Exp $ i*)
-
-(*#* Axiomatisation of a numerical set
-
- It will be instantiated by Z and R later on
- We choose to introduce many operation to allow flexibility in definition
- ([S] is primitive in the definition of [nat] while [add] and [one]
- are primitive in the definition
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/N.con *********************)
inline procedural "cic:/Coq/Num/Definitions/N.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/zero.con ******************)
+
inline procedural "cic:/Coq/Num/Definitions/zero.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/one.con *******************)
+
inline procedural "cic:/Coq/Num/Definitions/one.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/add.con *******************)
+
inline procedural "cic:/Coq/Num/Definitions/add.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/S.con *********************)
+
inline procedural "cic:/Coq/Num/Definitions/S.con".
-(*#* Relations *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/eq.con ********************)
inline procedural "cic:/Coq/Num/Definitions/eq.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/lt.con ********************)
+
inline procedural "cic:/Coq/Num/Definitions/lt.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/le.con ********************)
+
inline procedural "cic:/Coq/Num/Definitions/le.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/gt.con ********************)
+
inline procedural "cic:/Coq/Num/Definitions/gt.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/ge.con ********************)
+
inline procedural "cic:/Coq/Num/Definitions/ge.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/neq.con *******************)
+
inline procedural "cic:/Coq/Num/Definitions/neq.con" as definition.