diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/subtac/subtac_pretyping_F.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index 8456d24a99..a1d9603187 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -629,8 +629,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c = ise_pretype_gen false resolve_classes sigma env ([],[]) (OfType exptyp) c - let understand_tcc_evars evdref env kind c = - pretype_gen false true evdref env ([],[]) kind c + let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c = + pretype_gen fail_evar resolve_classes evdref env ([],[]) kind c end module Default : S = SubtacPretyping_F(Coercion.Default) |