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: GtAxioms.v,v 1.3 2002/02/14 14:39:02 filliatr Exp $ i*)
-
include "Num/Axioms.ma".
include "Num/LeProps.ma".
-(*#* Axiomatizing [>] from [<] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/GtAxioms/not_le_gt.con ****************)
inline procedural "cic:/Coq/Num/GtAxioms/not_le_gt.con".
-inline procedural "cic:/Coq/Num/GtAxioms/gt_not_le.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/GtAxioms/gt_not_le.con ****************)
-(* UNEXPORTED
-Hints Resolve not_le_gt : num.
-*)
-
-(* UNEXPORTED
-Hints Immediate gt_not_le : num.
-*)
+inline procedural "cic:/Coq/Num/GtAxioms/gt_not_le.con".