diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 5 | ||||
| -rw-r--r-- | plugins/syntax/float_syntax.ml | 4 |
2 files changed, 7 insertions, 2 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index e004613ef3..5d6e7c51d0 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -370,6 +370,11 @@ let ehole_var = EConstr.mkVar (Id.of_string "_") let pr_econstr_pat env sigma c0 = let rec wipe_evar c = let open EConstr in if isEvar sigma c then ehole_var else map sigma wipe_evar c in + let dummy_decl = + let dummy_prod = mkProd (make_annot Anonymous Sorts.Relevant,mkProp,mkProp) in + let na = make_annot (EConstr.destVar sigma ehole_var) Sorts.Relevant in + Context.Named.Declaration.(LocalAssum (na, dummy_prod)) in + let env = Environ.push_named dummy_decl env in pr_econstr_env env sigma (wipe_evar c0) (* Turn (new) evars into metas *) diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml index 9861a060ab..8e87fc13ca 100644 --- a/plugins/syntax/float_syntax.ml +++ b/plugins/syntax/float_syntax.ml @@ -28,8 +28,8 @@ let warn_inexact_float = Pp.strbrk (Printf.sprintf "The constant %s is not a binary64 floating-point value. \ - A closest value will be used and unambiguously printed %s." - sn (Float64.to_string f))) + A closest value %s will be used and unambiguously printed %s." + sn (Float64.to_hex_string f) (Float64.to_string f))) let interp_float ?loc n = let sn = NumTok.Signed.to_string n in |