diff options
Diffstat (limited to 'plugins/ring')
-rw-r--r-- | plugins/ring/LegacyArithRing.v | 2 | ||||
-rw-r--r-- | plugins/ring/LegacyNArithRing.v | 2 | ||||
-rw-r--r-- | plugins/ring/LegacyRing.v | 2 | ||||
-rw-r--r-- | plugins/ring/LegacyRing_theory.v | 2 | ||||
-rw-r--r-- | plugins/ring/LegacyZArithRing.v | 2 | ||||
-rw-r--r-- | plugins/ring/Ring_abstract.v | 2 | ||||
-rw-r--r-- | plugins/ring/Ring_normalize.v | 2 | ||||
-rw-r--r-- | plugins/ring/Setoid_ring.v | 2 | ||||
-rw-r--r-- | plugins/ring/Setoid_ring_normalize.v | 2 | ||||
-rw-r--r-- | plugins/ring/Setoid_ring_theory.v | 2 | ||||
-rw-r--r-- | plugins/ring/g_ring.ml4 | 2 | ||||
-rw-r--r-- | plugins/ring/ring.ml | 2 |
12 files changed, 12 insertions, 12 deletions
diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v index 27349683..3e30b90f 100644 --- a/plugins/ring/LegacyArithRing.v +++ b/plugins/ring/LegacyArithRing.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: LegacyArithRing.v 13323 2010-07-24 15:57:30Z herbelin $ *) (* Instantiation of the Ring tactic for the naturals of Arith $*) diff --git a/plugins/ring/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v index 7a2f4abc..337c3085 100644 --- a/plugins/ring/LegacyNArithRing.v +++ b/plugins/ring/LegacyNArithRing.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: LegacyNArithRing.v 13323 2010-07-24 15:57:30Z herbelin $ *) (* Instantiation of the Ring tactic for the binary natural numbers *) diff --git a/plugins/ring/LegacyRing.v b/plugins/ring/LegacyRing.v index 5ab90555..6b655134 100644 --- a/plugins/ring/LegacyRing.v +++ b/plugins/ring/LegacyRing.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: LegacyRing.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Export Bool. Require Export LegacyRing_theory. diff --git a/plugins/ring/LegacyRing_theory.v b/plugins/ring/LegacyRing_theory.v index 74d8f186..fb4c87fb 100644 --- a/plugins/ring/LegacyRing_theory.v +++ b/plugins/ring/LegacyRing_theory.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: LegacyRing_theory.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Export Bool. diff --git a/plugins/ring/LegacyZArithRing.v b/plugins/ring/LegacyZArithRing.v index 293ac12e..22fa87c8 100644 --- a/plugins/ring/LegacyZArithRing.v +++ b/plugins/ring/LegacyZArithRing.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: LegacyZArithRing.v 13323 2010-07-24 15:57:30Z herbelin $ *) (* Instantiation of the Ring tactic for the binary integers of ZArith *) diff --git a/plugins/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v index 96764e51..e65e1ce8 100644 --- a/plugins/ring/Ring_abstract.v +++ b/plugins/ring/Ring_abstract.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Ring_abstract.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Import LegacyRing_theory. Require Import Quote. diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v index 320e1ab2..d68fef4f 100644 --- a/plugins/ring/Ring_normalize.v +++ b/plugins/ring/Ring_normalize.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Ring_normalize.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Import LegacyRing_theory. Require Import Quote. diff --git a/plugins/ring/Setoid_ring.v b/plugins/ring/Setoid_ring.v index 15495071..3a3dfe84 100644 --- a/plugins/ring/Setoid_ring.v +++ b/plugins/ring/Setoid_ring.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Setoid_ring.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Export Setoid_ring_theory. Require Export Quote. diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v index 6bd5b419..6a53b519 100644 --- a/plugins/ring/Setoid_ring_normalize.v +++ b/plugins/ring/Setoid_ring_normalize.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Setoid_ring_normalize.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Import Setoid_ring_theory. Require Import Quote. diff --git a/plugins/ring/Setoid_ring_theory.v b/plugins/ring/Setoid_ring_theory.v index 96910db6..d55f25fc 100644 --- a/plugins/ring/Setoid_ring_theory.v +++ b/plugins/ring/Setoid_ring_theory.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Setoid_ring_theory.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Export Bool. Require Export Setoid. diff --git a/plugins/ring/g_ring.ml4 b/plugins/ring/g_ring.ml4 index dc34fdbc..7fda4920 100644 --- a/plugins/ring/g_ring.ml4 +++ b/plugins/ring/g_ring.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: g_ring.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Quote open Ring diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index fc2a04b3..3cdf0117 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: ring.ml 13323 2010-07-24 15:57:30Z herbelin $ *) (* ML part of the Ring tactic *) |