diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-21 12:36:19 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-21 12:36:19 +0000 |
| commit | 9024a91b59b9ecfb94e68b3748f2a9a66adcf515 (patch) | |
| tree | 44d3483d8ec18b2f8bba7a0a348632edbfad465c /intf | |
| parent | 47cbc272e79db52cc96dfe3d4d1cd4b978e4fa2a (diff) | |
Cutting the dependency of Genarg in constr_expr, glob_constr
related types. This will ultimately allow putting genargs into
these ASTs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16600 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index dbe888714..c253e888d 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -87,6 +87,18 @@ type ('a,'t) match_rule = | Pat of 'a match_context_hyps list * 'a match_pattern * 't | All of 't +(** Composite types *) + +(** In globalize tactics, we need to keep the initial [constr_expr] to recompute + in the environment by the effective calls to Intro, Inversion, etc + The [constr_expr] field is [None] in TacDef though *) +type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option + +type open_constr_expr = unit * constr_expr +type open_glob_constr = unit * glob_constr_and_expr + +type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern + (** Generic expressions for atomic tactics *) type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr = |