diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 5 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 3 |
2 files changed, 0 insertions, 8 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 7362b57fe4..40b8bcad92 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1194,11 +1194,6 @@ let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutT let (sigma, c) = ise_pretype_gen flags env sigma empty_lvar expected_type c in (sigma, c) -let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=WithoutTypeConstraint) c = - let sigma, c = ise_pretype_gen flags env !evdref empty_lvar expected_type c in - evdref := sigma; - c - let understand_ltac flags env sigma lvar kind c = let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in (sigma, c) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index aa25e36048..7395e94a09 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -55,9 +55,6 @@ val all_and_fail_flags : inference_flags val understand_tcc : ?flags:inference_flags -> env -> evar_map -> ?expected_type:typing_constraint -> glob_constr -> evar_map * constr -val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref -> - ?expected_type:typing_constraint -> glob_constr -> constr - (** More general entry point with evars from ltac *) (** Generic call to the interpreter from glob_constr to constr |