diff options
| author | Pierre-Marie Pédrot | 2018-10-26 13:50:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-26 13:50:12 +0200 |
| commit | 27266c1f79e565a6a19da4c79fc1ce83f748e31c (patch) | |
| tree | 865bd07aa81debed13d6c5b5f4b5b2d8d26d7443 /plugins | |
| parent | 69cbb9c09d5a440461b945c6690745b444649fda (diff) | |
| parent | 2e53939f4ce4bc06a5e7b621bc560d3ebeb59110 (diff) | |
Merge PR #8687: Mini reorganization type of global constr of global
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/table.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 7b4fd280bd..f6eea3c5c4 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -446,7 +446,7 @@ let error_MPfile_as_mod mp b = let argnames_of_global r = let env = Global.env () in - let typ, _ = Global.type_of_global_in_context env r in + let typ, _ = Typeops.type_of_global_in_context env r in let rels,_ = decompose_prod (Reduction.whd_all env typ) in List.rev_map fst rels @@ -878,7 +878,7 @@ let extract_constant_inline inline r ids s = match g with | ConstRef kn -> let env = Global.env () in - let typ, _ = Global.type_of_global_in_context env (ConstRef kn) in + let typ, _ = Typeops.type_of_global_in_context env (ConstRef kn) in let typ = Reduction.whd_all env typ in if Reduction.is_arity env typ then begin diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index a385a61ae0..28a9542167 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -311,7 +311,7 @@ let pr_info f_info = str "function_constant_type := " ++ (try Printer.pr_lconstr_env env sigma - (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant))) + (fst (Typeops.type_of_global_in_context env (ConstRef f_info.function_constant))) with e when CErrors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 876751911b..940defb743 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -360,7 +360,7 @@ let coerce_search_pattern_to_sort hpat = Pattern.PApp (fp, args') in let hr, na = splay_search_pattern 0 hpat in let dc, ht = - let hr, _ = Global.type_of_global_in_context (Global.env ()) hr (** FIXME *) in + let hr, _ = Typeops.type_of_global_in_context env hr (** FIXME *) in Reductionops.splay_prod env sigma (EConstr.of_constr hr) in let np = List.length dc in if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else |