From a3ab8b07b912afd1b883ed60bd532b5a29bccd8f Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 29 May 2012 11:09:01 +0000
Subject: Stuff about notation_constr (ex-aconstr) now in notation_ops.ml

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

(limited to 'plugins')

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 95c6a6d997..9fe77bf9d1 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1243,7 +1243,7 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b
 	   if array_for_all
 	     (fun l ->
 		let (n',nt',is_defined') = List.nth l i in
-		n = n' && Topconstr.eq_glob_constr nt nt' && is_defined = is_defined')
+		n = n' && Notation_ops.eq_glob_constr nt nt' && is_defined = is_defined')
 	     rels_params
 	   then
 	     l := param::!l
-- 
cgit v1.2.3