aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-09-15 18:10:48 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-01 17:57:37 +0200
commit569a26809a3b5e72033aac29e9e2bc91f74f2092 (patch)
treeece8ef50140da9c1f0719c0e1f25e11a7777b568 /pretyping
parenta92b0e3abb476743f6f12ce828a0d82eb3c98e98 (diff)
Remove understand_tcc_evars.
Use the functional interface understand_tcc instead.
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/pretyping.ml5
-rw-r--r--pretyping/pretyping.mli3
2 files changed, 0 insertions, 8 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 7362b57fe..40b8bcad9 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 aa25e3604..7395e94a0 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