From c7038a54f86d10a1205cad4733496e1b7de235b7 Mon Sep 17 00:00:00 2001
From: puech
Date: Fri, 29 Jul 2011 14:28:22 +0000
Subject: Const_omega: replaced some generic = on constr by eq_constr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14354 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/romega/const_omega.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'plugins')

diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index b6f6107194..e810e15c11 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -178,21 +178,21 @@ let coq_do_omega = lazy (constant  "do_omega")
 (* \subsection{Construction d'expressions} *)
 
 let do_left t =
-  if t = Lazy.force coq_c_nop then Lazy.force coq_c_nop
+  if Term.eq_constr t (Lazy.force coq_c_nop) then Lazy.force coq_c_nop
   else Term.mkApp (Lazy.force coq_c_do_left, [|t |] )
 
 let do_right t =
-  if t = Lazy.force coq_c_nop then Lazy.force coq_c_nop
+  if Term.eq_constr t (Lazy.force coq_c_nop) then Lazy.force coq_c_nop
   else Term.mkApp (Lazy.force coq_c_do_right, [|t |])
 
 let do_both t1 t2 =
-  if t1 = Lazy.force coq_c_nop then do_right t2
-  else if t2 = Lazy.force coq_c_nop then do_left t1
+  if Term.eq_constr t1 (Lazy.force coq_c_nop) then do_right t2
+  else if Term.eq_constr t2 (Lazy.force coq_c_nop) then do_left t1
   else Term.mkApp (Lazy.force coq_c_do_both , [|t1; t2 |])
 
 let do_seq t1 t2 =
-  if t1 = Lazy.force coq_c_nop then t2
-  else if t2 = Lazy.force coq_c_nop then t1
+  if Term.eq_constr t1 (Lazy.force coq_c_nop) then t2
+  else if Term.eq_constr t2 (Lazy.force coq_c_nop) then t1
   else Term.mkApp (Lazy.force coq_c_do_seq, [|t1; t2 |])
 
 let rec do_list = function
-- 
cgit v1.2.3