diff options
| author | Hugo Herbelin | 2018-10-09 20:47:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-19 16:55:40 +0200 |
| commit | 9b5ceabc9b62cdf9b806bb4abdff73642113e12e (patch) | |
| tree | 06a671e2a3b7867a6e8302a64c159362234ac344 /interp/notation.ml | |
| parent | 6a52d22067727da3d5b2128ea1ac67f8037138b1 (diff) | |
Deprecating Global.type_of_global_in_context.
Removing a few Global.env in the way.
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 6104ab16c7..db8ee5bc18 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1314,7 +1314,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) = | ArgsScopeNoDischarge -> assert false | ArgsScopeAuto -> let env = Global.env () in (*FIXME?*) - let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in + let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in let scs,cls = compute_arguments_scope_full sigma typ in (req,r,List.length scs,scs,cls) | ArgsScopeManual -> @@ -1322,7 +1322,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) = for the extra parameters of the section. Discard the classes of the manually given scopes to avoid further re-computations. *) let env = Global.env () in (*FIXME?*) - let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in + let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in let l',cls = compute_arguments_scope_full sigma typ in let l1 = List.firstn n l' in let cls1 = List.firstn n cls in @@ -1369,7 +1369,7 @@ let find_arguments_scope r = let declare_ref_arguments_scope sigma ref = let env = Global.env () in (* FIXME? *) - let typ = EConstr.of_constr @@ fst @@ Global.type_of_global_in_context env ref in + let typ = EConstr.of_constr @@ fst @@ Typeops.type_of_global_in_context env ref in let (scs,cls as o) = compute_arguments_scope_full sigma typ in declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o |