From fc3f8eb9bcb6645a97a35335d588dbd50231689b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 8 Apr 2008 16:15:23 +0000
Subject: - A little cleanup in Classes/*. Separate standard morphisms on
 relf/sym/trans relations from morphisms on prop connectives and relations. -
 Add general order theory on predicates, instantiated for relations. Derives
 equivalence, implication, conjunction and disjunction as liftings from
 propositional connectives. Can be used for n-ary homogeneous predicates
 thanks to a bit of metaprogramming with lists of types. - Rebind
 Setoid_Theory to use the Equivalence record type instead of declaring an
 isomorphic one. One needs to do "red" after constructor to get the same
 statements when building objects of type Setoid_Theory, so scripts break.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10765 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/setoid_ring/Ring_theory.v | 2 +-
 contrib/setoid_ring/newring.ml4   | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'contrib')

diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v
index cefdcf52b8..4c542ffdd7 100644
--- a/contrib/setoid_ring/Ring_theory.v
+++ b/contrib/setoid_ring/Ring_theory.v
@@ -257,7 +257,7 @@ Section ALMOST_RING.
 
  (** Leibniz equality leads to a setoid theory and is extensional*)
  Lemma Eqsth : Setoid_Theory R (@eq R).
- Proof.  constructor;intros;subst;trivial. Qed.
+ Proof.  constructor;red;intros;subst;trivial. Qed.
 
  Lemma Eq_s_ext : sring_eq_ext radd rmul (@eq R).
  Proof. constructor;intros;subst;trivial. Qed.
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 7cf642ce7e..c80b37d91f 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -527,7 +527,7 @@ let ring_equality (r,add,mul,opp,req) =
 	  (setoid,op_morph)
     | _ ->
 	let setoid = setoid_of_relation (Global.env ()) r req in
-	let signature = [Some (r,req);Some (r,req)],Some(r,req) in
+	let signature = [Some (r,req);Some (r,req)],Some(Lazy.lazy_from_val (r,req)) in
 	let add_m, add_m_lem =
 	  try Class_tactics.default_morphism signature add
           with Not_found ->
@@ -540,7 +540,7 @@ let ring_equality (r,add,mul,opp,req) =
           match opp with
             | Some opp ->
 		(let opp_m,opp_m_lem =
-		  try Class_tactics.default_morphism ([Some(r,req)],Some(r,req)) opp
+		  try Class_tactics.default_morphism ([Some(r,req)],Some(Lazy.lazy_from_val (r,req))) opp
 		  with Not_found ->
                     error "ring opposite should be declared as a morphism" in
 		let op_morph =
@@ -830,7 +830,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl =
 TACTIC EXTEND ring_lookup
 | [ "ring_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(lr)
       "[" constr(t) "]" ] ->
-          [ring_lookup (fst f) lH lr t]
+    [ring_lookup (fst f) lH lr t]
 END
 
 
@@ -1037,7 +1037,7 @@ let field_equality r inv req =
         mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|])
     | _ ->
 	let _setoid = setoid_of_relation (Global.env ()) r req in
-	let signature = [Some (r,req)],Some(r,req) in
+	let signature = [Some (r,req)],Some(Lazy.lazy_from_val (r,req)) in
 	let inv_m, inv_m_lem =
 	  try Class_tactics.default_morphism signature inv
           with Not_found ->
-- 
cgit v1.2.3