- 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

2 files changed, 5 insertions, 5 deletions

diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v
index cefdcf52b..4c542ffdd 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 7cf642ce7..c80b37d91 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 ->