From 574bdce32385d8c787db15e2df82dda3f838e48f Mon Sep 17 00:00:00 2001
From: puech
Date: Fri, 29 Jul 2011 14:26:07 +0000
Subject: Evarutil: generic equality on constr replaced by destructors

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14332 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarutil.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 0cf1594b5f..2e940583c6 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -933,7 +933,8 @@ let are_canonical_instances args1 args2 env =
     | [] ->
 	let rec aux2 n =
 	  n = n1 ||
-	  (args1.(n) = mkRel (n1-n) && args2.(n) = mkRel (n1-n) && aux2 (n+1))
+	  (isRel args1.(n) && destRel args1.(n) = n1-n &&
+	   isRel args2.(n) && destRel args2.(n) = n1-n && aux2 (n+1))
 	in aux2 n
     | _ -> false in
   n1 = n2 & aux 0 (named_context env)
-- 
cgit v1.2.3