diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/impargs.ml | 6 | ||||
| -rw-r--r-- | interp/notation.ml | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/interp/impargs.ml b/interp/impargs.ml index ce33cb8731..d8582d856e 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -450,13 +450,13 @@ let compute_mib_implicits flags kn = (Array.mapi (* No need to lift, arities contain no de Bruijn *) (fun i mip -> (** No need to care about constraints here *) - let ty, _ = Global.type_of_global_in_context env (IndRef (kn,i)) in + let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty)) mib.mind_packets) in let env_ar = Environ.push_rel_context ar env in let imps_one_inductive i mip = let ind = (kn,i) in - let ar, _ = Global.type_of_global_in_context env (IndRef ind) in + let ar, _ = Typeops.type_of_global_in_context env (IndRef ind) in ((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)), Array.mapi (fun j c -> (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c)) @@ -694,7 +694,7 @@ let declare_manual_implicits local ref ?enriching l = let flags = !implicit_args in let env = Global.env () in let sigma = Evd.from_env env in - let t, _ = Global.type_of_global_in_context env ref in + let t, _ = Typeops.type_of_global_in_context env ref in let t = of_constr t in let enriching = Option.default flags.auto enriching in let autoimpls = compute_auto_implicits env sigma flags enriching t in 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 |