From 5dcafa956e49eefc451dd021a0fe8ad2e2338088 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 15 Aug 2014 17:43:35 +0200
Subject: Lazy interpretation of patterns so that expressions such as "intros H
 H'/H" can be given with second H bound by the first one.

Not very satisfied by passing closure to tactics.ml, but otherwise
tactics would have to be aware of glob_constr.
---
 printing/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing/pptactic.ml')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 5ea4293c9b..8c3e9a7e01 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1024,7 +1024,7 @@ let () =
     Constrarg.wit_intro_pattern
     (Miscprint.pr_intro_pattern pr_constr_expr)
     (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
-    (Miscprint.pr_intro_pattern pr_constr);
+    (Miscprint.pr_intro_pattern (fun c -> pr_constr (snd (c (Global.env()) Evd.empty))));
   Genprint.register_print0
     Constrarg.wit_clause_dft_concl
     (pr_clauses (Some true) pr_lident)
-- 
cgit v1.2.3