From 133516a1acebebfce527204fe5109a5eecb9bb45 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 19 May 2008 17:45:32 +0000
Subject: Fix globalization bug in class_tactics and refactorize instance
 declaration code.

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

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 618d48482a..dacdf2052a 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -1338,7 +1338,7 @@ let add_morphism_infer m n =
 		    add_instance (Typeclasses.new_instance (Lazy.force morphism_class) None false cst);
 		    declare_projection n instance_id (ConstRef cst)
 		| _ -> assert false);
-	    Pfedit.by (Tacinterp.interp <:tactic<add_morphism_tactic>>)) ();
+	    Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) ();
 	Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) () 
 
 let add_morphism binders m s n =
-- 
cgit v1.2.3