summaryrefslogtreecommitdiff
path: root/contrib/ring
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/ring')
-rw-r--r--contrib/ring/LegacyRing.v2
-rw-r--r--contrib/ring/LegacyRing_theory.v6
-rw-r--r--contrib/ring/Ring_abstract.v4
-rw-r--r--contrib/ring/Ring_normalize.v6
-rw-r--r--contrib/ring/Setoid_ring_normalize.v4
-rw-r--r--contrib/ring/Setoid_ring_theory.v8
-rw-r--r--contrib/ring/quote.ml9
-rw-r--r--contrib/ring/ring.ml20
8 files changed, 32 insertions, 27 deletions
diff --git a/contrib/ring/LegacyRing.v b/contrib/ring/LegacyRing.v
index dc8635bd..40323b3d 100644
--- a/contrib/ring/LegacyRing.v
+++ b/contrib/ring/LegacyRing.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Ring.v 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id: LegacyRing.v 10739 2008-04-01 14:45:20Z herbelin $ *)
Require Export Bool.
Require Export LegacyRing_theory.
diff --git a/contrib/ring/LegacyRing_theory.v b/contrib/ring/LegacyRing_theory.v
index 5df927a6..d15d18a6 100644
--- a/contrib/ring/LegacyRing_theory.v
+++ b/contrib/ring/LegacyRing_theory.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: LegacyRing_theory.v 9179 2006-09-26 12:13:06Z barras $ *)
+(* $Id: LegacyRing_theory.v 9370 2006-11-13 09:21:31Z herbelin $ *)
Require Export Bool.
@@ -153,7 +153,7 @@ Notation "- x" := (Aopp x).
Record Ring_Theory : Prop :=
{Th_plus_comm : forall n m:A, n + m = m + n;
Th_plus_assoc : forall n m p:A, n + (m + p) = n + m + p;
- Th_mult_sym : forall n m:A, n * m = m * n;
+ Th_mult_comm : forall n m:A, n * m = m * n;
Th_mult_assoc : forall n m p:A, n * (m * p) = n * m * p;
Th_plus_zero_left : forall n:A, 0 + n = n;
Th_mult_one_left : forall n:A, 1 * n = n;
@@ -165,7 +165,7 @@ Variable T : Ring_Theory.
Let plus_comm := Th_plus_comm T.
Let plus_assoc := Th_plus_assoc T.
-Let mult_comm := Th_mult_sym T.
+Let mult_comm := Th_mult_comm T.
Let mult_assoc := Th_mult_assoc T.
Let plus_zero_left := Th_plus_zero_left T.
Let mult_one_left := Th_mult_one_left T.
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index 115ed5ca..c2467ebf 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Ring_abstract.v 9179 2006-09-26 12:13:06Z barras $ *)
+(* $Id: Ring_abstract.v 9370 2006-11-13 09:21:31Z herbelin $ *)
Require Import LegacyRing_theory.
Require Import Quote.
@@ -428,7 +428,7 @@ Fixpoint interp_ap (p:apolynomial) : A :=
Hint Resolve (Th_plus_comm T).
Hint Resolve (Th_plus_assoc T).
Hint Resolve (Th_plus_assoc2 T).
-Hint Resolve (Th_mult_sym T).
+Hint Resolve (Th_mult_comm T).
Hint Resolve (Th_mult_assoc T).
Hint Resolve (Th_mult_assoc2 T).
Hint Resolve (Th_plus_zero_left T).
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index 4a082396..e8d9f1ee 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Ring_normalize.v 9179 2006-09-26 12:13:06Z barras $ *)
+(* $Id: Ring_normalize.v 10913 2008-05-09 14:40:04Z herbelin $ *)
Require Import LegacyRing_theory.
Require Import Quote.
@@ -774,7 +774,7 @@ Variable T : Ring_Theory Aplus Amult Aone Azero Aopp Aeq.
Hint Resolve (Th_plus_comm T).
Hint Resolve (Th_plus_assoc T).
Hint Resolve (Th_plus_assoc2 T).
-Hint Resolve (Th_mult_sym T).
+Hint Resolve (Th_mult_comm T).
Hint Resolve (Th_mult_assoc T).
Hint Resolve (Th_mult_assoc2 T).
Hint Resolve (Th_plus_zero_left T).
@@ -897,6 +897,6 @@ End rings.
Infix "+" := Pplus : ring_scope.
Infix "*" := Pmult : ring_scope.
Notation "- x" := (Popp x) : ring_scope.
-Notation "[ x ]" := (Pvar x) (at level 1) : ring_scope.
+Notation "[ x ]" := (Pvar x) (at level 0) : ring_scope.
Delimit Scope ring_scope with ring.
diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v
index 56329ade..8eb49a37 100644
--- a/contrib/ring/Setoid_ring_normalize.v
+++ b/contrib/ring/Setoid_ring_normalize.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Setoid_ring_normalize.v 6662 2005-02-02 21:33:14Z sacerdot $ *)
+(* $Id: Setoid_ring_normalize.v 9370 2006-11-13 09:21:31Z herbelin $ *)
Require Import Setoid_ring_theory.
Require Import Quote.
@@ -1032,7 +1032,7 @@ Variable T : Setoid_Ring_Theory Aequiv Aplus Amult Aone Azero Aopp Aeq.
Hint Resolve (STh_plus_comm T).
Hint Resolve (STh_plus_assoc T).
Hint Resolve (STh_plus_assoc2 S T).
-Hint Resolve (STh_mult_sym T).
+Hint Resolve (STh_mult_comm T).
Hint Resolve (STh_mult_assoc T).
Hint Resolve (STh_mult_assoc2 S T).
Hint Resolve (STh_plus_zero_left T).
diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v
index ae6610d3..88abd7de 100644
--- a/contrib/ring/Setoid_ring_theory.v
+++ b/contrib/ring/Setoid_ring_theory.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Setoid_ring_theory.v 6662 2005-02-02 21:33:14Z sacerdot $ *)
+(* $Id: Setoid_ring_theory.v 10631 2008-03-06 18:17:24Z msozeau $ *)
Require Export Bool.
Require Export Setoid.
@@ -177,7 +177,7 @@ Section Theory_of_setoid_rings.
Record Setoid_Ring_Theory : Prop :=
{STh_plus_comm : forall n m:A, n + m == m + n;
STh_plus_assoc : forall n m p:A, n + (m + p) == n + m + p;
- STh_mult_sym : forall n m:A, n * m == m * n;
+ STh_mult_comm : forall n m:A, n * m == m * n;
STh_mult_assoc : forall n m p:A, n * (m * p) == n * m * p;
STh_plus_zero_left : forall n:A, 0 + n == n;
STh_mult_one_left : forall n:A, 1 * n == n;
@@ -189,7 +189,7 @@ Variable T : Setoid_Ring_Theory.
Let plus_comm := STh_plus_comm T.
Let plus_assoc := STh_plus_assoc T.
-Let mult_comm := STh_mult_sym T.
+Let mult_comm := STh_mult_comm T.
Let mult_assoc := STh_mult_assoc T.
Let plus_zero_left := STh_plus_zero_left T.
Let mult_one_left := STh_mult_one_left T.
@@ -245,7 +245,7 @@ Lemma Saux1 : forall a:A, a + a == a -> a == 0.
intros.
rewrite <- (plus_zero_left a).
rewrite (plus_comm 0 a).
-setoid_replace (a + 0) with (a + (a + - a)); auto.
+setoid_replace (a + 0) with (a + (a + - a)) by auto.
rewrite (plus_assoc a a (- a)).
rewrite H.
apply opp_def.
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index e0a6cba3..7cd22a36 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: quote.ml 9178 2006-09-26 11:18:22Z barras $ *)
+(* $Id: quote.ml 10790 2008-04-14 22:34:19Z herbelin $ *)
(* The `Quote' tactic *)
@@ -191,8 +191,11 @@ let decomp_term c = kind_of_term (strip_outer_cast c)
?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive
type [typ] *)
-let coerce_meta_out id = int_of_string (string_of_id id)
-let coerce_meta_in n = id_of_string (string_of_int n)
+let coerce_meta_out id =
+ let s = string_of_id id in
+ int_of_string (String.sub s 1 (String.length s - 1))
+let coerce_meta_in n =
+ id_of_string ("M" ^ string_of_int n)
let compute_lhs typ i nargsi =
match kind_of_term typ with
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 6b82b75b..3d13a254 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -6,13 +6,13 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ring.ml 9179 2006-09-26 12:13:06Z barras $ *)
+(* $Id: ring.ml 11094 2008-06-10 19:35:23Z herbelin $ *)
(* ML part of the Ring tactic *)
open Pp
open Util
-open Options
+open Flags
open Term
open Names
open Libnames
@@ -193,7 +193,7 @@ let _ =
let subst_morph subst morph =
let plusm' = subst_mps subst morph.plusm in
let multm' = subst_mps subst morph.multm in
- let oppm' = option_smartmap (subst_mps subst) morph.oppm in
+ let oppm' = Option.smartmap (subst_mps subst) morph.oppm in
if plusm' == morph.plusm
&& multm' == morph.multm
&& oppm' == morph.oppm then
@@ -215,15 +215,15 @@ let subst_set subst cset =
if !same then cset else cset'
let subst_theory subst th =
- let th_equiv' = option_smartmap (subst_mps subst) th.th_equiv in
- let th_setoid_th' = option_smartmap (subst_mps subst) th.th_setoid_th in
- let th_morph' = option_smartmap (subst_morph subst) th.th_morph in
+ let th_equiv' = Option.smartmap (subst_mps subst) th.th_equiv in
+ let th_setoid_th' = Option.smartmap (subst_mps subst) th.th_setoid_th in
+ let th_morph' = Option.smartmap (subst_morph subst) th.th_morph in
let th_a' = subst_mps subst th.th_a in
let th_plus' = subst_mps subst th.th_plus in
let th_mult' = subst_mps subst th.th_mult in
let th_one' = subst_mps subst th.th_one in
let th_zero' = subst_mps subst th.th_zero in
- let th_opp' = option_smartmap (subst_mps subst) th.th_opp in
+ let th_opp' = Option.smartmap (subst_mps subst) th.th_opp in
let th_eq' = subst_mps subst th.th_eq in
let th_t' = subst_mps subst th.th_t in
let th_closed' = subst_set subst th.th_closed in
@@ -826,9 +826,11 @@ let raw_polynom th op lc gl =
c'''i; ci; c'i_eq_c''i |]))))
(tclTHENS
(tclORELSE
- (Setoid_replace.general_s_rewrite true c'i_eq_c''i
+ (Setoid_replace.general_s_rewrite true
+ Termops.all_occurrences c'i_eq_c''i
~new_goals:[])
- (Setoid_replace.general_s_rewrite false c'i_eq_c''i
+ (Setoid_replace.general_s_rewrite false
+ Termops.all_occurrences c'i_eq_c''i
~new_goals:[]))
[tac]))
else
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 08:44:05 +0000