diff options
Diffstat (limited to 'interp/tactypes.ml')
| -rw-r--r-- | interp/tactypes.ml | 32 |
1 files changed, 30 insertions, 2 deletions
diff --git a/interp/tactypes.ml b/interp/tactypes.ml index 83e42be89..f19abefee 100644 --- a/interp/tactypes.ml +++ b/interp/tactypes.ml @@ -15,7 +15,35 @@ open Names open Constrexpr open Pattern -open Misctypes + +(** Introduction patterns *) + +type 'constr intro_pattern_expr = + | IntroForthcoming of bool + | IntroNaming of Namegen.intro_pattern_naming_expr + | IntroAction of 'constr intro_pattern_action_expr +and 'constr intro_pattern_action_expr = + | IntroWildcard + | IntroOrAndPattern of 'constr or_and_intro_pattern_expr + | IntroInjection of ('constr intro_pattern_expr) CAst.t list + | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t + | IntroRewrite of bool +and 'constr or_and_intro_pattern_expr = + | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list + | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list + +(** Bindings *) + +type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t + +type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list + +type 'a bindings = + | ImplicitBindings of 'a list + | ExplicitBindings of 'a explicit_bindings + | NoBindings + +type 'a with_bindings = 'a * 'a bindings (** In globalize tactics, we need to keep the initial [constr_expr] to recompute in the environment by the effective calls to Intro, Inversion, etc @@ -31,4 +59,4 @@ type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_op type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t -type intro_pattern_naming = intro_pattern_naming_expr CAst.t +type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t |