diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index b6fea7dc20..08004e9718 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -18,6 +18,7 @@ open Declarations open Inductive open Reduction open Environ +open Libnames open Declare open Refiner open Tacmach @@ -314,7 +315,7 @@ let general_elim_then_using | _ -> let name_elim = match kind_of_term elim with - | Const sp -> string_of_path sp + | Const kn -> string_of_kn kn | Var id -> string_of_id id | _ -> "\b" in |