From 5143129baac805d3a49ac3ee9f3344c7a447634f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 30 Oct 2016 17:53:07 +0100
Subject: Termops API using EConstr.

---
 printing/printer.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 3c8ad4255c..b36df27ed3 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 *)
-- 
cgit v1.2.3