diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 4 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 26706321b5..545f8931f2 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -597,7 +597,7 @@ let build_scheme fas = (fun (_,f,sort) -> let f_as_constant = try - match Nametab.global f with + match Smartlocate.global_with_alias f with | Globnames.ConstRef c -> c | _ -> Errors.error "Functional Scheme can only be used with functions" with Not_found -> @@ -629,7 +629,7 @@ let build_case_scheme fa = (* Constrintern.global_reference id *) (* in *) let funs = (fun (_,f,_) -> - try fst (Universes.unsafe_constr_of_global (Nametab.global f)) + try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f)) with Not_found -> Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in let first_fun,u = destConst funs in diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 6e46d36253..71da59c499 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -215,7 +215,7 @@ VERNAC COMMAND EXTEND NewFunctionalScheme | (_,fun_name,_)::_ -> begin begin - make_graph (Nametab.global fun_name) + make_graph (Smartlocate.global_with_alias fun_name) end ; try Functional_principles_types.build_scheme fas @@ -245,7 +245,7 @@ END (***** debug only ***) VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY -["Generate" "graph" "for" reference(c)] -> [ make_graph (Nametab.global c) ] +["Generate" "graph" "for" reference(c)] -> [ make_graph (Smartlocate.global_with_alias c) ] END diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 0d254c9af7..72613624ba 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1266,7 +1266,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp let hook _ _ = let opacity = let na_ref = Libnames.Ident (Loc.ghost,na) in - let na_global = Nametab.global na_ref in + let na_global = Smartlocate.global_with_alias na_ref in match na_global with ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant") |