From 71563ebb86a83bc7cdfc17f58493f59428d764b0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 12 Jul 2017 14:49:26 +0200 Subject: Safer API for constr_of_global, and getting rid of unsafe_constr_of_global. --- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/recdef.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 8c9b514e6..d726c1a2b 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -651,7 +651,7 @@ let build_case_scheme fa = (* in *) let funs = let (_,f,_) = fa in - try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f)) + try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f)) with Not_found -> user_err ~hdr:"FunInd.build_case_scheme" (str "Cannot find " ++ Libnames.pr_reference f) in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 1705cac78..bc550c8b9 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -90,7 +90,7 @@ let type_of_const sigma t = |_ -> assert false let constr_of_global x = - fst (Universes.unsafe_constr_of_global x) + fst (Global.constr_of_global_in_context (Global.env ()) x) let constant sl s = constr_of_global (find_reference sl s) -- cgit v1.2.3