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.
---
 intf/tacexpr.mli | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 9b75282ca1..abb2292cd1 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -106,9 +106,16 @@ type open_glob_constr = unit * glob_constr_and_expr
 
 type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
 
-type intro_pattern = Term.constr intro_pattern_expr located
-type intro_patterns = Term.constr intro_pattern_expr located list
-type or_and_intro_pattern = Term.constr or_and_intro_pattern_expr located
+type delayed_open_constr_with_bindings =
+    Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr with_bindings
+
+type delayed_open_constr =
+    Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr
+
+type intro_pattern = delayed_open_constr intro_pattern_expr located
+type intro_patterns = delayed_open_constr intro_pattern_expr located list
+type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located
+type intro_pattern_naming = intro_pattern_naming_expr located
 
 (** Generic expressions for atomic tactics *)
 
-- 
cgit v1.2.3