diff options
| author | Pierre-Marie Pédrot | 2016-03-04 15:04:35 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-04 15:37:34 +0100 |
| commit | 098d283e58966124cfe0e97a3229a9e7e6284120 (patch) | |
| tree | 9ffc61382b3b66a6da24276fd15b14175f21e887 /intf | |
| parent | d5656a6c28f79d59590d4fde60c5158a649d1b65 (diff) | |
Removing the UConstr entry of the tactic_arg AST.
This was redundant with the wit_uconstr generic argument, so there was no real
point on keeping it there.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 7366bc03e6..f2a567c00d 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -180,7 +180,6 @@ type 'a gen_atomic_tactic_expr = constraint 'a = < term:'trm; - utrm: 'utrm; dterm: 'dtrm; pattern:'pat; constant:'cst; @@ -195,7 +194,6 @@ constraint 'a = < and 'a gen_tactic_arg = | TacGeneric of 'lev generic_argument | ConstrMayEval of ('trm,'cst,'pat) may_eval - | UConstr of 'utrm | Reference of 'ref | TacCall of Loc.t * 'ref * 'a gen_tactic_arg list @@ -206,7 +204,6 @@ and 'a gen_tactic_arg = constraint 'a = < term:'trm; - utrm: 'utrm; dterm: 'dtrm; pattern:'pat; constant:'cst; @@ -285,7 +282,6 @@ and 'a gen_tactic_expr = constraint 'a = < term:'t; - utrm: 'utrm; dterm: 'dtrm; pattern:'p; constant:'c; @@ -300,7 +296,6 @@ and 'a gen_tactic_fun_ast = constraint 'a = < term:'t; - utrm: 'utrm; dterm: 'dtrm; pattern:'p; constant:'c; @@ -313,7 +308,6 @@ constraint 'a = < (** Globalized tactics *) type g_trm = glob_constr_and_expr -type g_utrm = g_trm type g_pat = glob_constr_pattern_and_expr type g_cst = evaluable_global_reference and_short_name or_var type g_ref = ltac_constant located or_var @@ -321,7 +315,6 @@ type g_nam = Id.t located type g_dispatch = < term:g_trm; - utrm:g_utrm; dterm:g_trm; pattern:g_pat; constant:g_cst; @@ -343,7 +336,6 @@ type glob_tactic_arg = (** Raw tactics *) type r_trm = constr_expr -type r_utrm = r_trm type r_pat = constr_pattern_expr type r_cst = reference or_by_notation type r_ref = reference @@ -352,7 +344,6 @@ type r_lev = rlevel type r_dispatch = < term:r_trm; - utrm:r_utrm; dterm:r_trm; pattern:r_pat; constant:r_cst; @@ -374,7 +365,6 @@ type raw_tactic_arg = (** Interpreted tactics *) type t_trm = Term.constr -type t_utrm = Glob_term.closed_glob_constr type t_pat = constr_pattern type t_cst = evaluable_global_reference type t_ref = ltac_constant located @@ -382,7 +372,6 @@ type t_nam = Id.t type t_dispatch = < term:t_trm; - utrm:t_utrm; dterm:g_trm; pattern:t_pat; constant:t_cst; |