From 6cf2f61e672f1a0aa6c06589d8b64c7958167a62 Mon Sep 17 00:00:00 2001
From: puech
Date: Fri, 29 Jul 2011 14:27:50 +0000
Subject: Quote: replaced generic = on constr by eq_constr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14349 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/quote/quote.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 41d92b2331..a81392ad41 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -370,7 +370,7 @@ let rec subterm gl (t : constr) (t' : constr) =
 let rec sort_subterm gl l =
   let rec insert c = function
     | [] -> [c]
-    | (h::t as l) when c = h -> l (* Avoid doing the same work twice *)
+    | (h::t as l) when eq_constr c h -> l (* Avoid doing the same work twice *)
     | h::t -> if subterm gl c h then c::h::t else h::(insert c t)
   in
   match l with
-- 
cgit v1.2.3