diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-15 18:10:48 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-01 17:57:37 +0200 |
| commit | 569a26809a3b5e72033aac29e9e2bc91f74f2092 (patch) | |
| tree | ece8ef50140da9c1f0719c0e1f25e11a7777b568 /pretyping/pretyping.ml | |
| parent | a92b0e3abb476743f6f12ce828a0d82eb3c98e98 (diff) | |
Remove understand_tcc_evars.
Use the functional interface understand_tcc instead.
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 5 |
1 files changed, 0 insertions, 5 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) |