diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 857e82fc59..7fbc1b9819 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1258,7 +1258,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant") in - let lemma = mkConst (Lib.make_con na) in + let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in ref_ := Some lemma ; let lid = ref [] in let h_num = ref (-1) in |