diff options
Diffstat (limited to 'src/tac2expr.mli')
| -rw-r--r-- | src/tac2expr.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/tac2expr.mli b/src/tac2expr.mli index 0b9923f7b9..bbe127e94d 100644 --- a/src/tac2expr.mli +++ b/src/tac2expr.mli @@ -188,6 +188,10 @@ type frame = type backtrace = frame list +type ('a, _) arity = +| OneAty : ('a, 'a -> 'a Proofview.tactic) arity +| AddAty : ('a, 'b) arity -> ('a, 'a -> 'b) arity + type valexpr = | ValInt of int (** Immediate integers *) @@ -202,7 +206,7 @@ type valexpr = | ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr (** Arbitrary data *) -and ml_tactic = valexpr list -> valexpr Proofview.tactic +and ml_tactic = MLTactic : (valexpr, 'v) arity * 'v -> ml_tactic type environment = { env_ist : valexpr Id.Map.t; |