diff options
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 20abde82f2..8e12b239e8 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -30,7 +30,7 @@ open Nametab open Declare open Decl_kinds open Tacred -open Proof_type +open Goal open Pfedit open Glob_term open Pretyping @@ -1295,7 +1295,7 @@ let is_opaque_constant c = let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) - let current_proof_name = get_current_proof_name () in + let current_proof_name = Proof_global.get_current_proof_name () in let name = match goal_name with | Some s -> s | None -> |