From 2015ca9f06f02f4a22653600dec676fc68dd83f7 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 2 Sep 2009 20:46:09 +0000
Subject: Stop unnecessary use of lazy values for constraints, simplifying
 setoid_rewrite's code. Cleanup in vernacexpr.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12303 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/setoid_ring/newring.ml4 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 14fd9192e9..6d1ed511b7 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -533,7 +533,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(Lazy.lazy_from_val (r,req)) in
+	let signature = [Some (r,req);Some (r,req)],Some(r,req) in
 	let add_m, add_m_lem =
 	  try Rewrite.default_morphism signature add
           with Not_found ->
@@ -546,7 +546,7 @@ let ring_equality (r,add,mul,opp,req) =
           match opp with
             | Some opp ->
 		(let opp_m,opp_m_lem =
-		  try Rewrite.default_morphism ([Some(r,req)],Some(Lazy.lazy_from_val (r,req))) opp
+		  try Rewrite.default_morphism ([Some(r,req)],Some(r,req)) opp
 		  with Not_found ->
                     error "ring opposite should be declared as a morphism" in
 		let op_morph =
@@ -1035,7 +1035,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(Lazy.lazy_from_val (r,req)) in
+	let signature = [Some (r,req)],Some(r,req) in
 	let inv_m, inv_m_lem =
 	  try Rewrite.default_morphism signature inv
           with Not_found ->
-- 
cgit v1.2.3