diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-12 15:55:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 15:14:45 +0200 |
| commit | 469a9b3242891b089b4a211e96b5b568277f7fc0 (patch) | |
| tree | bd6854ea387f33192bf3d44c6d729e5d23471f49 /interp/notation.ml | |
| parent | 34bcd562cc9c8e5e6b0f3b79a15b9c55dd98813e (diff) | |
Remove the function Global.type_of_global_unsafe.
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 4067a6b94..c07a00943 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -718,13 +718,13 @@ let rebuild_arguments_scope (req,r,n,l,_) = match req with | ArgsScopeNoDischarge -> assert false | ArgsScopeAuto -> - let scs,cls = compute_arguments_scope_full (fst(Universes.type_of_global r)(*FIXME?*)) in + let scs,cls = compute_arguments_scope_full (fst(Global.type_of_global_in_context (Global.env ()) r)(*FIXME?*)) in (req,r,List.length scs,scs,cls) | ArgsScopeManual -> (* Add to the manually given scopes the one found automatically for the extra parameters of the section. Discard the classes of the manually given scopes to avoid further re-computations. *) - let l',cls = compute_arguments_scope_full (Global.type_of_global_unsafe r) in + let l',cls = compute_arguments_scope_full (fst (Global.type_of_global_in_context (Global.env ()) r)) in let l1 = List.firstn n l' in let cls1 = List.firstn n cls in (req,r,0,l1@l,cls1) @@ -768,7 +768,7 @@ let find_arguments_scope r = with Not_found -> [] let declare_ref_arguments_scope ref = - let t = Global.type_of_global_unsafe ref in + let t, _ = Global.type_of_global_in_context (Global.env ()) ref in let (scs,cls as o) = compute_arguments_scope_full t in declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o |