diff options
Diffstat (limited to 'contrib/setoid_ring/NArithRing.v')
| -rw-r--r-- | contrib/setoid_ring/NArithRing.v | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/contrib/setoid_ring/NArithRing.v b/contrib/setoid_ring/NArithRing.v deleted file mode 100644 index 0ba519fd..00000000 --- a/contrib/setoid_ring/NArithRing.v +++ /dev/null @@ -1,21 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Export Ring. -Require Import BinPos BinNat. -Import InitialRing. - -Set Implicit Arguments. - -Ltac Ncst t := - match isNcst t with - true => t - | _ => constr:NotConstant - end. - -Add Ring Nr : Nth (decidable Neq_bool_ok, constants [Ncst]). |