diff options
| author | msozeau | 2008-05-19 17:45:32 +0000 |
|---|---|---|
| committer | msozeau | 2008-05-19 17:45:32 +0000 |
| commit | 133516a1acebebfce527204fe5109a5eecb9bb45 (patch) | |
| tree | 759a9e2c8fe200b85a02be81b8e2d366424de8ac /tactics | |
| parent | 3f4cadb34000a931fc59dc21047444a1c044d76a (diff) | |
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
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
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 = |