diff options
| author | msozeau | 2009-06-22 18:28:18 +0000 |
|---|---|---|
| committer | msozeau | 2009-06-22 18:28:18 +0000 |
| commit | 604a07a7d425aa4b89bcd391c083d8600c71c5b5 (patch) | |
| tree | fb6a3b161207b062eda89a58fbd54519b89c2427 /plugins | |
| parent | b0a8a08682c8f9c8f3457adef403c48f8fc011ac (diff) | |
Fixes for r12197, the refined evars were not returned in case fail_evar
was true.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12206 85f007b7-540e-0410-9357-904b9bb8a0f7
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) |