diff options
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 3c8ad4255..b36df27ed 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -760,7 +760,8 @@ let pr_prim_rule = function str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]") | Refine c -> - str(if Termops.occur_meta c then "refine " else "exact ") ++ + (** FIXME *) + str(if Termops.occur_meta Evd.empty (EConstr.of_constr c) then "refine " else "exact ") ++ Constrextern.with_meta_as_hole pr_constr c (* Backwards compatibility *) |