diff options
author | 2016-09-15 17:03:39 +0200 | |
---|---|---|
committer | 2017-08-01 17:20:51 +0200 | |
commit | 533c4f693a557c81a13edc6e624ccaa9578c0ddc (patch) | |
tree | e0f6144da9195b8d94a738b90e4b578631ea0216 | |
parent | 9d5b26370a530be4267d07c5bd6e7cf4618f0e4b (diff) |
Remove understand_judgment and understand_judgment_tcc.
-rw-r--r-- | pretyping/pretyping.ml | 23 | ||||
-rw-r--r-- | pretyping/pretyping.mli | 9 |
2 files changed, 0 insertions, 32 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 72e51190b..156e61ab6 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1177,29 +1177,6 @@ let no_classes_no_fail_inference_flags = { let all_and_fail_flags = default_inference_flags true let all_no_fail_flags = default_inference_flags false -let on_judgment sigma f j = - let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in - let (c,_,t) = destCast sigma (f c) in - {uj_val = c; uj_type = t} - -let understand_judgment env sigma c = - let env = make_env env sigma in - let evdref = ref sigma in - let k0 = Context.Rel.length (rel_context env) in - let j = pretype k0 true empty_tycon env evdref empty_lvar c in - let j = on_judgment sigma (fun c -> - let evd, c = process_inference_flags all_and_fail_flags env.ExtraEnv.env sigma (!evdref,c) in - evdref := evd; c) j - in j, Evd.evar_universe_context !evdref - -let understand_judgment_tcc env evdref c = - let env = make_env env !evdref in - let k0 = Context.Rel.length (rel_context env) in - let j = pretype k0 true empty_tycon env evdref empty_lvar c in - on_judgment !evdref (fun c -> - let (evd,c) = process_inference_flags all_no_fail_flags env.ExtraEnv.env Evd.empty (!evdref,c) in - evdref := evd; c) j - let ise_pretype_gen_ctx flags env sigma lvar kind c = let evd, c = ise_pretype_gen flags env sigma lvar kind c in let evd, f = Evarutil.nf_evars_and_universes evd in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 66ca59152..c475bcf7e 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -84,15 +84,6 @@ val understand_ltac : inference_flags -> val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> env -> evar_map -> glob_constr -> Constr.constr Evd.in_evar_universe_context -(** Idem but returns the judgment of the understood term *) - -val understand_judgment : env -> evar_map -> - glob_constr -> unsafe_judgment Evd.in_evar_universe_context - -(** Idem but do not fail on unresolved evars (type cl*) -val understand_judgment_tcc : env -> evar_map ref -> - glob_constr -> unsafe_judgment - val type_uconstr : ?flags:inference_flags -> ?expected_type:typing_constraint -> |